let f1, f2 be Function of NAT ,(bool the carrier of T); :: thesis: ( ( for n being Element of NAT
for B being Subset of T st B = f1 . n holds
f1 . (n + 1) = B ^d ) & f1 . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = f2 . n holds
f2 . (n + 1) = B ^d ) & f2 . 0 = A implies f1 = f2 )
assume that
A2: ( ( for n being Element of NAT
for B being Subset of T st B = f1 . n holds
f1 . (n + 1) = B ^d ) & f1 . 0 = A ) and
A3: ( ( for n being Element of NAT
for B being Subset of T st B = f2 . n holds
f2 . (n + 1) = B ^d ) & f2 . 0 = A ) ; :: thesis: f1 = f2
defpred S₁[ Element of NAT ] means f1 . $1 = f2 . $1;
A4: dom f1 = NAT by FUNCT_2:def 1;
then A5: dom f1 = dom f2 by FUNCT_2:def 1;
for n being Element of NAT holds S₁[n]

proof

A6: S₁[ 0 ] by A2, A3;
A7: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A8: S₁[n] ; :: thesis: S₁[n + 1]
reconsider B1 = f1 . n as Subset of T ;
B1 ^d = f1 . (n + 1) by A2;
hence S₁[n + 1] by A3, A8; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A6, A7);
hence for n being Element of NAT holds S₁[n] ; :: thesis: verum

end;

then for x being set st x in dom f1 holds
f1 . x = f2 . x by A4;
hence f1 = f2 by A5, FUNCT_1:9; :: thesis: verum