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

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

end;