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 & 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 ) ) ) ; :: 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 A4: ( T = G . n & G . 0 = Imf X,X & ( 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;
A5: S₁[ 0 ] by A3, A4;
A6: 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 A7: F . k = G . k ; :: thesis: S₁[k + 1]
consider Q being RMembership_Func of X,X such that
A8: ( G . k = Q & G . (k + 1) = Q (#) R ) by A4;
consider Q' being RMembership_Func of X,X such that
A9: ( F . k = Q' & F . (k + 1) = Q' (#) R ) by A3;
thus S₁[k + 1] by A7, A8, A9; :: thesis: verum

end;

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