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

proof

let a be Element of ; :: 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