let T be non empty RelStr ; :: thesis: for A being Subset of T holds Fdfl (A,2) = (A ^d) ^d
let A be Subset of T; :: thesis: Fdfl (A,2) = (A ^d) ^d
Fdfl (A,2) = Fdfl (A,(1 + 1))
.= (Fdfl (A,1)) ^d by Def8 ;
hence Fdfl (A,2) = (A ^d) ^d by Th40; :: thesis: verum