reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
set D = the carrier of (FuzzyLattice [:X,X:]);
defpred S₁[ set , set , set ] means ex Q being Element of the carrier of (FuzzyLattice [:X,X:]) st
( $2 = Q & $3 = (@ Q) (#) R );
A1: for k being Nat
for x being Element of the carrier of (FuzzyLattice [:X,X:]) ex y being Element of the carrier of (FuzzyLattice [:X,X:]) st S₁[k,x,y]

proof

let k be Nat; :: thesis: for x being Element of the carrier of (FuzzyLattice [:X,X:]) ex y being Element of the carrier of (FuzzyLattice [:X,X:]) st S₁[k,x,y]
let Q be Element of the carrier of (FuzzyLattice [:X,X:]); :: thesis: ex y being Element of the carrier of (FuzzyLattice [:X,X:]) st S₁[k,Q,y]
set y = (@ Q) (#) R;
reconsider y9 = ([:X,X:],((@ Q) (#) R)) @ as Element of the carrier of (FuzzyLattice [:X,X:]) ;
take y9 ; :: thesis: S₁[k,Q,y9]
thus S₁[k,Q,y9] by LFUZZY_0:def 6; :: thesis: verum

end;

consider F being sequence of the carrier of (FuzzyLattice [:X,X:]) such that
A2: ( F . 0 = ([:X,X:],(Imf (X,X))) @ & ( for k being Nat holds S₁[k,F . k,F . (k + 1)] ) ) from RECDEF_1:sch 2(A1);
reconsider F = F as sequence of (Funcs ([:X,X:],[.0,1.])) by LFUZZY_0:14;
reconsider IT = F . n9 as Element of (FuzzyLattice [:X,X:]) 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 A2, LFUZZY_0:def 6; :: 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 (FuzzyLattice [:X,X:]) 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
S₁[n,F . n,F . (n + 1)] by A2;
hence F . (k + 1) = Q (#) R ; :: thesis: verum

end;

end;