let X, Y, Z be non empty set ; for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
let R be RMembership_Func of X,Y; for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
let S be RMembership_Func of Y,Z; for x being Element of X
for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
let x be Element of X; for z being Element of Z
for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
let z be Element of Z; for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
let a be Element of (RealPoset [.0,1.]); a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
set A = { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ;
set B = { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ;
for b being object holds
( b in { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } iff b in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } )
proof
let b be
object ;
( b in { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } iff b in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } )
hereby ( b in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } implies b in { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } )
assume
b in { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum }
;
b in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } then consider y being
Element of
Y such that A1:
b = (a "/\" (R . (x,y))) "/\" (S . (y,z))
;
b = ((R . (x,y)) "/\" (S . (y,z))) "/\" a
by A1, LATTICE3:16;
hence
b in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum }
;
verum
end;
assume
b in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum }
;
b in { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum }
then consider y being
Element of
Y such that A2:
b = ((R . (x,y)) "/\" (S . (y,z))) "/\" a
;
b = (a "/\" (R . (x,y))) "/\" (S . (y,z))
by A2, LATTICE3:16;
hence
b in { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum }
;
verum
end;
then
{ ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } = { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum }
by TARSKI:2;
hence
a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
by Lm5; verum