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 S1[ Nat] means F . $1 = G . $1;
A9: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A10: F . k = G . k ; :: thesis: S1[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 S1[k + 1] by A10; :: thesis: verum
end;
A11: S1[ 0 ] by A4, A7;
for k being Nat holds S1[k] from NAT_1:sch 2(A11, A9);
 hence S = T by A3, A6; :: thesis: verum