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 ^f ) & f1 . 0 = A & ( for n being Nat
for B being Subset of T st B = f2 . n holds
f2 . (n + 1) = B ^f ) & 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 ^f 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 ^f and
A5: f2 . 0 = A ; :: thesis: f1 = f2
defpred S₁[ Nat] means f1 . $1 = f2 . $1;
A6: dom f1 = NAT by FUNCT_2:def 1;
then A7: dom f1 = dom f2 by FUNCT_2:def 1;
for n being Nat holds S₁[n]

proof

let n be Nat; :: thesis: S₁[n]
A8: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

end;

A10: S₁[ 0 ] by A3, A5;
for m being Nat holds S₁[m] from NAT_1:sch 2(A10, A8);
hence S₁[n] ; :: thesis: verum

end;

then for x being object st x in dom f1 holds
f1 . x = f2 . x by A6;
hence f1 = f2 by A7, FUNCT_1:2; :: thesis: verum