let X, Y, Z be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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.]); :: thesis: 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 } )

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; :: thesis: verum

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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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.]); :: thesis: 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

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;
let b be object ; :: thesis: ( 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 } )

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 } ; :: thesis: verum

end;hereby :: thesis: ( 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 { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum }
; :: thesis: 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 }
; :: thesis: 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 } ; :: thesis: verum

end;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 } ; :: thesis: 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 } ; :: thesis: verum

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; :: thesis: verum