let X be non empty set ; :: thesis: for Q being Subset of (FuzzyLattice X)
for x being Element of X holds ("\/" (Q,(FuzzyLattice X))) . x = "\/" ((pi (Q,x)),(RealPoset [.0,1.]))
let Q be Subset of (FuzzyLattice X); :: thesis: for x being Element of X holds ("\/" (Q,(FuzzyLattice X))) . x = "\/" ((pi (Q,x)),(RealPoset [.0,1.]))
let x be Element of X; :: thesis: ("\/" (Q,(FuzzyLattice X))) . x = "\/" ((pi (Q,x)),(RealPoset [.0,1.]))
A1: for a being Element of X holds (X --> (RealPoset [.0,1.])) . a is complete LATTICE by FUNCOP_1:7;
FuzzyLattice X = (RealPoset [.0,1.]) |^ X by LFUZZY_0:def 4
.= product (X --> (RealPoset [.0,1.])) by YELLOW_1:def 5 ;
then (sup Q) . x = "\/" ((pi (Q,x)),((X --> (RealPoset [.0,1.])) . x)) by A1, WAYBEL_3:32;
hence ("\/" (Q,(FuzzyLattice X))) . x = "\/" ((pi (Q,x)),(RealPoset [.0,1.])) by FUNCOP_1:7; :: thesis: verum