reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
set D = the carrier of ();
defpred S1[ set , set , set ] means ex Q being Element of the carrier of () st
( \$2 = Q & \$3 = (@ Q) (#) R );
A1: for k being Nat
for x being Element of the carrier of () ex y being Element of the carrier of () st S1[k,x,y]
proof
let k be Nat; :: thesis: for x being Element of the carrier of () ex y being Element of the carrier of () st S1[k,x,y]
let Q be Element of the carrier of (); :: thesis: ex y being Element of the carrier of () st S1[k,Q,y]
set y = (@ Q) (#) R;
reconsider y9 = ([:X,X:],((@ Q) (#) R)) @ as Element of the carrier of () ;
take y9 ; :: thesis: S1[k,Q,y9]
thus S1[k,Q,y9] by LFUZZY_0:def 6; :: thesis: verum
end;
consider F being sequence of the carrier of () such that
A2: ( F . 0 = ([:X,X:],(Imf (X,X))) @ & ( for k being Nat holds S1[k,F . k,F . (k + 1)] ) ) from reconsider F = F as sequence of (Funcs ([:X,X:],[.0,1.])) by LFUZZY_0:14;
reconsider IT = F . n9 as Element of () by LFUZZY_0:14;
reconsider IT9 = @ IT as RMembership_Func of X,X ;
take IT9 ; :: thesis: ex F being sequence of (Funcs ([:X,X:],[.0,1.])) st
( IT9 = 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 ) ) )

thus ex F being sequence of (Funcs ([:X,X:],[.0,1.])) st
( IT9 = 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 ) ) ) :: thesis: verum
proof
take F ; :: thesis: ( IT9 = 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 ) ) )

thus IT9 = F . n by LFUZZY_0:def 5; :: thesis: ( 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 ) ) )

thus F . 0 = Imf (X,X) by ; :: thesis: for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R )

thus for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) :: thesis: verum
proof
let k be Nat; :: thesis: ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R )

reconsider n = k as Element of NAT by ORDINAL1:def 12;
reconsider Q9 = F . n as Element of the carrier of () by LFUZZY_0:14;
reconsider Q = @ Q9 as RMembership_Func of X,X ;
take Q ; :: thesis: ( F . k = Q & F . (k + 1) = Q (#) R )
thus F . k = Q by LFUZZY_0:def 5; :: thesis: F . (k + 1) = Q (#) R
S1[n,F . n,F . (n + 1)] by A2;
hence F . (k + 1) = Q (#) R ; :: thesis: verum
end;
end;