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 ((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; 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; 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; 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; 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.]); ((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 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 } } ;
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
let c be
object ;
( 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 } )
hereby ( 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 { (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 } }
;
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;
verum
end;
assume
c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum }
;
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 } }
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;
verum
end;
((R (#) S) . (x,z)) "/\" a =
("\/" ( { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) "/\" a
by Th22
.=
"\/" ( { (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; verum