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

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
(Fint (A /\ B)) . (k + 1) = (Fint (A /\ B),k) ^i by Def4
.= ((Fint A,k) ^i ) /\ ((Fint B,k) ^i ) by A2, Th10
.= (Fint A,(k + 1)) /\ ((Fint B,k) ^i ) by Def4
.= ((Fint A) . (k + 1)) /\ ((Fint B) . (k + 1)) by Def4 ;
hence S₁[k + 1] ; :: thesis: verum

end;

(Fint (A /\ B)) . 0 = A /\ B by Def4
.= ((Fint A) . 0 ) /\ B by Def4
.= ((Fint A) . 0 ) /\ ((Fint B) . 0 ) by Def4 ;
then A3: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A1);
hence Fint (A /\ B),n = (Fint A,n) /\ (Fint B,n) ; :: thesis: verum