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 ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) 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 ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) 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 ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) 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 ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) 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 ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.]))

let a be Element of (RealPoset [.0,1.]); :: thesis: ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.]))

A1: { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } c= the carrier of (RealPoset [.0,1.])

set B = { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ;

A2: for c being object holds

( c in { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } iff c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } )

.= "\/" ( { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } ,(RealPoset [.0,1.])) by A1, Th15 ;

hence ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.])) by A2, TARSKI:2; :: 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 ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) 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 ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) 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 ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) 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 ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) 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 ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.]))

let a be Element of (RealPoset [.0,1.]); :: thesis: ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.]))

A1: { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } c= the carrier of (RealPoset [.0,1.])

proof

set A = { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } ;
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } or d in the carrier of (RealPoset [.0,1.]) )

assume d in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ; :: thesis: d in the carrier of (RealPoset [.0,1.])

then ex t being Element of Y st d = (R . (x,t)) "/\" (S . (t,z)) ;

hence d in the carrier of (RealPoset [.0,1.]) ; :: thesis: verum

end;assume d in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ; :: thesis: d in the carrier of (RealPoset [.0,1.])

then ex t being Element of Y st d = (R . (x,t)) "/\" (S . (t,z)) ;

hence d in the carrier of (RealPoset [.0,1.]) ; :: thesis: verum

set B = { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ;

A2: for c being object holds

( c in { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } iff c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } )

proof

((R (#) S) . (x,z)) "/\" a =
("\/" ( { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) "/\" a
by Th22
let c be object ; :: thesis: ( c in { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } iff c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } )

then consider y being Element of Y such that

A5: c = ((R . (x,y)) "/\" (S . (y,z))) "/\" a ;

(R . (x,y)) "/\" (S . (y,z)) in { ((R . (x,y1)) "/\" (S . (y1,z))) where y1 is Element of Y : verum } ;

hence c in { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } by A5; :: thesis: verum

end;hereby :: thesis: ( c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } implies c in { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } )

assume
c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum }
; :: thesis: c in { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } assume
c in { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } }
; :: thesis: c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum }

then consider b being Element of (RealPoset [.0,1.]) such that

A3: c = b "/\" a and

A4: b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ;

ex y being Element of Y st b = (R . (x,y)) "/\" (S . (y,z)) by A4;

hence c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } by A3; :: thesis: verum

end;then consider b being Element of (RealPoset [.0,1.]) such that

A3: c = b "/\" a and

A4: b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ;

ex y being Element of Y st b = (R . (x,y)) "/\" (S . (y,z)) by A4;

hence c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } by A3; :: thesis: verum

then consider y being Element of Y such that

A5: c = ((R . (x,y)) "/\" (S . (y,z))) "/\" a ;

(R . (x,y)) "/\" (S . (y,z)) in { ((R . (x,y1)) "/\" (S . (y1,z))) where y1 is Element of Y : verum } ;

hence c in { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } by A5; :: thesis: verum

.= "\/" ( { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } ,(RealPoset [.0,1.])) by A1, Th15 ;

hence ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.])) by A2, TARSKI:2; :: thesis: verum