let C1, C2 be Subset of (E ^omega); ( ex concat being sequence of (bool (E ^omega)) st
( C1 = concat . n & concat . 0 = {(<%> E)} & ( for i being Nat holds concat . (i + 1) = (concat . i) ^^ A ) ) & ex concat being sequence of (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 sequence of (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
; ( for concat being sequence of (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 sequence of (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
; C1 = C2
defpred S1[ Nat] means f1 . $1 = f2 . $1;
A10:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A11:
S1[
k]
;
S1[k + 1]
f2 . (k + 1) = (f2 . k) ^^ A
by A9;
hence
S1[
k + 1]
by A6, A11;
verum end;
A12:
S1[ 0 ]
by A5, A8;
for k being Nat holds S1[k]
from NAT_1:sch 2(A12, A10);
hence
C1 = C2
by A4, A7; verum