let C be non empty set ; :: thesis: for f, g being Membership_Func of C holds
( ( for c being Element of C holds f . c <= g . c ) iff C,f @ <<= C,g @ )
let f, g be Membership_Func of C; :: thesis: ( ( for c being Element of C holds f . c <= g . c ) iff C,f @ <<= C,g @ )
A1: (RealPoset [.0 ,1.]) |^ C = product (C --> (RealPoset [.0 ,1.])) by YELLOW_1:def 5;
A2: ( ( for c being Element of C holds f . c <= g . c ) implies C,f @ <<= C,g @ )

proof

assume A3: for c being Element of C holds f . c <= g . c ; :: thesis: C,f @ <<= C,g @
set f' = C,f @ ;
set g' = C,g @ ;
reconsider f' = C,f @ , g' = C,g @ as Element of (product (C --> (RealPoset [.0 ,1.]))) by YELLOW_1:def 5;
for c being Element of C holds f' . c <<= g' . c

proof

let c be Element of C; :: thesis: f' . c <<= g' . c
A4: (C --> (RealPoset [.0 ,1.])) . c = RealPoset [.0 ,1.] by FUNCOP_1:13;
set f1 = f . c;
set g1 = g . c;
( f . c <= g . c & f = f' & g = g' ) by A3;
hence f' . c <<= g' . c by A4, Th3; :: thesis: verum

end;

hence C,f @ <<= C,g @ by A1, WAYBEL_3:28; :: thesis: verum

end;

( C,f @ <<= C,g @ implies for c being Element of C holds f . c <= g . c )

proof

assume A5: C,f @ <<= C,g @ ; :: thesis: for c being Element of C holds f . c <= g . c
reconsider ff = C,f @ , gg = C,g @ as Element of (product (C --> (RealPoset [.0 ,1.]))) by YELLOW_1:def 5;
let c be Element of C; :: thesis: f . c <= g . c
A6: (C --> (RealPoset [.0 ,1.])) . c = RealPoset [.0 ,1.] by FUNCOP_1:13;
( ff . c <<= gg . c & C,f @ = f & C,g @ = g ) by A1, A5, WAYBEL_3:28;
hence f . c <= g . c by A6, Th3; :: thesis: verum

end;

hence ( ( for c being Element of C holds f . c <= g . c ) iff C,f @ <<= C,g @ ) by A2; :: thesis: verum