let f1, f2 be sequence of (bool the carrier of T); :: thesis: ( ( for n being Nat
for B being Subset of T st B = f1 . n holds
f1 . (n + 1) = B ^d ) & f1 . 0 = A & ( for n being 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 Nat
for B being Subset of T st B = f1 . n holds
f1 . (n + 1) = B ^d and
A3: f1 . 0 = A and
A4: for n being Nat
for B being Subset of T st B = f2 . n holds
f2 . (n + 1) = B ^d and
A5: f2 . 0 = A ; :: thesis: f1 = f2
defpred S₁[ Nat] means f1 . $1 = f2 . $1;
A6: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

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

end;

A8: dom f1 = NAT by FUNCT_2:def 1;
then A9: dom f1 = dom f2 by FUNCT_2:def 1;
A10: S₁[ 0 ] by A3, A5;
for n being Nat holds S₁[n] from NAT_1:sch 2(A10, A6);
then for x being object st x in dom f1 holds
f1 . x = f2 . x by A8;
hence f1 = f2 by A9, FUNCT_1:2; :: thesis: verum