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 A5: ( C1 = f1 . n & f1 . 0 = {(<%> E)} & ( 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 A6: ( C2 = f2 . n & f2 . 0 = {(<%> E)} & ( for i being Nat holds f2 . (i + 1) = (f2 . i) ^^ A ) ) ; :: thesis: C1 = C2
defpred S₁[ Nat] means f1 . $1 = f2 . $1;
A7: S₁[ 0 ] by A5, A6;

A8: now

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

end;

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