let C1, C2 be Subset of (E ^omega); :: thesis: ( ex concat being Function of NAT,(bool (E ^omega)) st
( C1 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) & ex concat being Function of NAT,(bool (E ^omega)) st
( C2 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) implies C1 = C2 )
given f1 being Function of NAT,(bool (E ^omega)) such that A4: C1 = f1 . n and
A5: f1 . 0 = {(<%> E)} and
A6: for i being Nat holds f1 . (i + 1) = (f1 . i) ^^ A ; :: thesis: ( for concat being Function of NAT,(bool (E ^omega)) holds
( not C2 = concat . n or not concat . 0 = {(<%> E)} or ex i being Nat st not concat . (i + 1) = (concat . i) ^^ A ) or C1 = C2 )
given f2 being Function of NAT,(bool (E ^omega)) such that A7: C2 = f2 . n and
A8: f2 . 0 = {(<%> E)} and
A9: for i being Nat holds f2 . (i + 1) = (f2 . i) ^^ A ; :: thesis: C1 = C2
defpred S₁[ Nat] means f1 . $1 = f2 . $1;

A10: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A11: S₁[k] ; :: thesis: S₁[k + 1]
f2 . (k + 1) = (f2 . k) ^^ A by A9;
hence S₁[k + 1] by A6, A11; :: thesis: verum

end;

A12: S₁[ 0 ] by A5, A8;
for k being Nat holds S₁[k] from NAT_1:sch 2(A12, A10);
hence C1 = C2 by A4, A7; :: thesis: verum