let A be non empty set ; :: thesis: FuzzyLattice A is constituted-Functions

for a being Element of (FuzzyLattice A) holds a is Function

for a being Element of (FuzzyLattice A) holds a is Function

proof

hence
FuzzyLattice A is constituted-Functions
by MONOID_0:def 1; :: thesis: verum
let a be Element of (FuzzyLattice A); :: thesis: a is Function

a in the carrier of (FuzzyLattice A) ;

then a in Funcs (A,[.0,1.]) by Th14;

then ex f being Function st

( a = f & dom f = A & rng f c= [.0,1.] ) by FUNCT_2:def 2;

hence a is Function ; :: thesis: verum

end;a in the carrier of (FuzzyLattice A) ;

then a in Funcs (A,[.0,1.]) by Th14;

then ex f being Function st

( a = f & dom f = A & rng f c= [.0,1.] ) by FUNCT_2:def 2;

hence a is Function ; :: thesis: verum