let S, T be RMembership_Func of X,X; :: thesis: ( ex F being Function of NAT ,(Funcs [:X,X:],[.0 ,1.]) st
( S = F . n & F . 0 = Imf X,X & ( for k being natural number ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) & ex F being Function of NAT ,(Funcs [:X,X:],[.0 ,1.]) st
( T = F . n & F . 0 = Imf X,X & ( for k being natural number ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) implies S = T )
given F being Function of NAT ,(Funcs [:X,X:],[.0 ,1.]) such that A3: S = F . n and
A4: F . 0 = Imf X,X and
A5: for k being natural number ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ; :: thesis: ( for F being Function of NAT ,(Funcs [:X,X:],[.0 ,1.]) holds
( not T = F . n or not F . 0 = Imf X,X or ex k being natural number 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 Function of NAT ,(Funcs [:X,X:],[.0 ,1.]) such that A6: T = G . n and
A7: G . 0 = Imf X,X and
A8: for k being natural number ex Q being RMembership_Func of X,X st
( G . k = Q & G . (k + 1) = Q (#) R ) ; :: thesis: S = T
defpred S₁[ natural number ] means F . $1 = G . $1;
A9: for k being natural number st S₁[k] holds
S₁[k + 1]

proof

let k be natural number ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A10: F . k = G . k ; :: thesis: S₁[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₁[k + 1] by A10; :: thesis: verum

end;

A11: S₁[ 0 ] by A4, A7;
for k being natural number holds S₁[k] from NAT_1:sch 2(A11, A9);
hence S = T by A3, A6; :: thesis: verum