let S, T be RMembership_Func of X,X; :: thesis: ( ex F being sequence of (Funcs ([:X,X:],[.0,1.])) st

( S = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st

( F . k = Q & F . (k + 1) = Q (#) R ) ) ) & ex F being sequence of (Funcs ([:X,X:],[.0,1.])) st

( T = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st

( F . k = Q & F . (k + 1) = Q (#) R ) ) ) implies S = T )

given F being sequence of (Funcs ([:X,X:],[.0,1.])) such that A3: S = F . n and

A4: F . 0 = Imf (X,X) and

A5: for k being Nat ex Q being RMembership_Func of X,X st

( F . k = Q & F . (k + 1) = Q (#) R ) ; :: thesis: ( for F being sequence of (Funcs ([:X,X:],[.0,1.])) holds

( not T = F . n or not F . 0 = Imf (X,X) or ex k being Nat st

for Q being RMembership_Func of X,X holds

( not F . k = Q or not F . (k + 1) = Q (#) R ) ) or S = T )

given G being sequence of (Funcs ([:X,X:],[.0,1.])) such that A6: T = G . n and

A7: G . 0 = Imf (X,X) and

A8: for k being Nat ex Q being RMembership_Func of X,X st

( G . k = Q & G . (k + 1) = Q (#) R ) ; :: thesis: S = T

defpred S_{1}[ Nat] means F . $1 = G . $1;

A9: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by A4, A7;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A11, A9);

hence S = T by A3, A6; :: thesis: verum

( S = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st

( F . k = Q & F . (k + 1) = Q (#) R ) ) ) & ex F being sequence of (Funcs ([:X,X:],[.0,1.])) st

( T = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st

( F . k = Q & F . (k + 1) = Q (#) R ) ) ) implies S = T )

given F being sequence of (Funcs ([:X,X:],[.0,1.])) such that A3: S = F . n and

A4: F . 0 = Imf (X,X) and

A5: for k being Nat ex Q being RMembership_Func of X,X st

( F . k = Q & F . (k + 1) = Q (#) R ) ; :: thesis: ( for F being sequence of (Funcs ([:X,X:],[.0,1.])) holds

( not T = F . n or not F . 0 = Imf (X,X) or ex k being Nat st

for Q being RMembership_Func of X,X holds

( not F . k = Q or not F . (k + 1) = Q (#) R ) ) or S = T )

given G being sequence of (Funcs ([:X,X:],[.0,1.])) such that A6: T = G . n and

A7: G . 0 = Imf (X,X) and

A8: for k being Nat ex Q being RMembership_Func of X,X st

( G . k = Q & G . (k + 1) = Q (#) R ) ; :: thesis: S = T

defpred S

A9: for k being Nat st S

S

proof

A11:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A10: F . k = G . k ; :: thesis: S_{1}[k + 1]

( ex Q being RMembership_Func of X,X st

( G . k = Q & G . (k + 1) = Q (#) R ) & ex Q9 being RMembership_Func of X,X st

( F . k = Q9 & F . (k + 1) = Q9 (#) R ) ) by A5, A8;

hence S_{1}[k + 1]
by A10; :: thesis: verum

end;assume A10: F . k = G . k ; :: thesis: S

( ex Q being RMembership_Func of X,X st

( G . k = Q & G . (k + 1) = Q (#) R ) & ex Q9 being RMembership_Func of X,X st

( F . k = Q9 & F . (k + 1) = Q9 (#) R ) ) by A5, A8;

hence S

for k being Nat holds S

hence S = T by A3, A6; :: thesis: verum