reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

set D = the carrier of (FuzzyLattice [:X,X:]);

defpred S_{1}[ 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_{1}[k,x,y]

A2: ( F . 0 = ([:X,X:],(Imf (X,X))) @ & ( for k being Nat holds S_{1}[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

set D = the carrier of (FuzzyLattice [:X,X:]);

defpred S

( $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

proof

consider F being sequence of the carrier of (FuzzyLattice [:X,X:]) such that
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_{1}[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_{1}[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_{1}[k,Q,y9]

thus S_{1}[k,Q,y9]
by LFUZZY_0:def 6; :: thesis: verum

end;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

set y = (@ Q) (#) R;

reconsider y9 = ([:X,X:],((@ Q) (#) R)) @ as Element of the carrier of (FuzzyLattice [:X,X:]) ;

take y9 ; :: thesis: S

thus S

A2: ( F . 0 = ([:X,X:],(Imf (X,X))) @ & ( for k being Nat holds S

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

end;( 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_{1}[n,F . n,F . (n + 1)]
by A2;

hence F . (k + 1) = Q (#) R ; :: thesis: verum

end;( 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

hence F . (k + 1) = Q (#) R ; :: thesis: verum