let T be non empty RelStr ; :: thesis: for A being Subset of T holds Fint A,1 = A ^i
let A be Subset of T; :: thesis: Fint A,1 = A ^i
A1: ( ( for n being Element of NAT
for B being Subset of T st B = (Fint A) . n holds
(Fint A) . (n + 1) = B ^i ) & (Fint A) . 0 = A ) by Def4;
for B being Subset of T st B = (Fint A) . 0 holds
(Fint A) . (0 + 1) = B ^i by Def4;
hence Fint A,1 = A ^i by A1; :: thesis: verum