let T be non empty RelStr ; :: thesis: for A, B being Subset of T
for n being Nat holds Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n))
let A, B be Subset of T; :: thesis: for n being Nat holds Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n))
defpred S₁[ Nat] means (Fdfl (A /\ B)) . $1 = ((Fdfl A) . $1) /\ ((Fdfl B) . $1);
let n be Nat; :: thesis: Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n))
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
(Fdfl (A /\ B)) . (k + 1) = (Fdfl ((A /\ B),k)) ^d by Def8
.= ((Fdfl (A,k)) ^d) /\ ((Fdfl (B,k)) ^d) by A2, Th12
.= (Fdfl (A,(k + 1))) /\ ((Fdfl (B,k)) ^d) by Def8
.= ((Fdfl A) . (k + 1)) /\ ((Fdfl B) . (k + 1)) by Def8 ;
hence S₁[k + 1] ; :: thesis: verum

end;

(Fdfl (A /\ B)) . 0 = A /\ B by Def8
.= ((Fdfl A) . 0) /\ B by Def8
.= ((Fdfl A) . 0) /\ ((Fdfl B) . 0) by Def8 ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n)) ; :: thesis: verum