let A be non empty set ; :: thesis: FuzzyLattice A is constituted-Functions
for a being Element of (FuzzyLattice A) holds a is Function

proof

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;

hence FuzzyLattice A is constituted-Functions by MONOID_0:def 1; :: thesis: verum