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 Element of 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 Element of 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 y' = [:X,X:],((@ Q) (#) R) @ as Element of the carrier of (FuzzyLattice [:X,X:]) ;
take y' ; :: thesis: S₁[k,Q,y']
thus S₁[k,Q,y'] by LFUZZY_0:def 6; :: thesis: verum

end;

consider F being Function of NAT ,the carrier of (FuzzyLattice [:X,X:]) such that
A2: ( F . 0 = [:X,X:],(Imf X,X) @ & ( for k being Element of NAT holds S₁[k,F . k,F . (k + 1)] ) ) from RECDEF_1:sch 2(A1);
Funcs [:X,X:],[.0 ,1.] = the carrier of (FuzzyLattice [:X,X:]) by LFUZZY_0:14;
then reconsider F = F as Function of NAT ,(Funcs [:X,X:],[.0 ,1.]) ;
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
reconsider IT = F . n' as Element of (FuzzyLattice [:X,X:]) by LFUZZY_0:14;
reconsider IT' = @ IT as RMembership_Func of X,X ;
take IT' ; :: thesis: ex F being Function of NAT ,(Funcs [:X,X:],[.0 ,1.]) st
( IT' = 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 ) ) )
thus ex F being Function of NAT ,(Funcs [:X,X:],[.0 ,1.]) st
( IT' = 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: verum

proof

take F ; :: thesis: ( IT' = 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 ) ) )
thus IT' = F . n by LFUZZY_0:def 5; :: thesis: ( 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 ) ) )
thus F . 0 = Imf X,X by A2, LFUZZY_0:def 6; :: thesis: for k being natural number ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R )
thus for k being natural number ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) :: thesis: verum

proof

let k be natural number ; :: 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 13;
reconsider Q' = F . n as Element of the carrier of (FuzzyLattice [:X,X:]) by LFUZZY_0:14;
reconsider Q = @ Q' 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;