let X, Y, Z, W be non empty set ; for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for T being RMembership_Func of Z,W holds (R (#) S) (#) T = R (#) (S (#) T)
let R be RMembership_Func of X,Y; for S being RMembership_Func of Y,Z
for T being RMembership_Func of Z,W holds (R (#) S) (#) T = R (#) (S (#) T)
let S be RMembership_Func of Y,Z; for T being RMembership_Func of Z,W holds (R (#) S) (#) T = R (#) (S (#) T)
let T be RMembership_Func of Z,W; (R (#) S) (#) T = R (#) (S (#) T)
A1:
for x, w being object st x in X & w in W holds
((R (#) S) (#) T) . (x,w) = (R (#) (S (#) T)) . (x,w)
proof
let x,
w be
object ;
( x in X & w in W implies ((R (#) S) (#) T) . (x,w) = (R (#) (S (#) T)) . (x,w) )
assume that A2:
x in X
and A3:
w in W
;
((R (#) S) (#) T) . (x,w) = (R (#) (S (#) T)) . (x,w)
reconsider w =
w as
Element of
W by A3;
reconsider x =
x as
Element of
X by A2;
set A =
{ ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) where z is Element of Z : verum } ;
set B =
{ (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum } ;
set C =
{ ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum } ;
set D =
{ ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } ;
defpred S1[
set ]
means verum;
deffunc H1(
Element of
Y,
Element of
Z)
-> Element of the
carrier of
(RealPoset [.0,1.]) =
((R . (x,$1)) "/\" (S . ($1,$2))) "/\" (T . ($2,w));
A4:
for
a being
object holds
(
a in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) where z is Element of Z : verum } iff
a in { (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum } )
proof
let a be
object ;
( a in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) where z is Element of Z : verum } iff a in { (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum } )
hereby ( a in { (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum } implies a in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) where z is Element of Z : verum } )
assume
a in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) where z is Element of Z : verum }
;
a in { (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum } then consider z being
Element of
Z such that A5:
a = "\/" (
{ (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,
(RealPoset [.0,1.]))
;
a = ((R (#) S) . (x,z)) "/\" (T . (z,w))
by A5, Lm5;
hence
a in { (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum }
;
verum
end;
assume
a in { (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum }
;
a in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) where z is Element of Z : verum }
then consider z being
Element of
Z such that A6:
a = ((R (#) S) . (x,z)) "/\" (T . (z,w))
;
a = "\/" (
{ (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,
(RealPoset [.0,1.]))
by A6, Lm5;
hence
a in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) where z is Element of Z : verum }
;
verum
end;
A7:
for
y being
Element of
Y for
z being
Element of
Z st
S1[
y] &
S1[
z] holds
H1(
y,
z)
= H1(
y,
z)
;
A8:
"\/" (
{ ("\/" ( { H1(y,z) where z is Element of Z : S1[z] } ,(RealPoset [.0,1.]))) where y is Element of Y : S1[y] } ,
(RealPoset [.0,1.]))
= "\/" (
{ ("\/" ( { H1(y1,z1) where y1 is Element of Y : S1[y1] } ,(RealPoset [.0,1.]))) where z1 is Element of Z : S1[z1] } ,
(RealPoset [.0,1.]))
from LFUZZY_0:sch 5(A7);
for
c being
object holds
(
c in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum } iff
c in { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } )
proof
let c be
object ;
( c in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum } iff c in { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } )
hereby ( c in { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } implies c in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum } )
assume
c in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum }
;
c in { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } then consider y being
Element of
Y such that A9:
c = "\/" (
{ (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,
(RealPoset [.0,1.]))
;
c = (R . (x,y)) "/\" ((S (#) T) . (y,w))
by A9, Lm6;
hence
c in { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum }
;
verum
end;
assume
c in { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum }
;
c in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum }
then consider y being
Element of
Y such that A10:
c = (R . (x,y)) "/\" ((S (#) T) . (y,w))
;
c = "\/" (
{ (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,
(RealPoset [.0,1.]))
by A10, Lm6;
hence
c in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum }
;
verum
end;
then A11:
{ ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum } = { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum }
by TARSKI:2;
(
((R (#) S) (#) T) . (
x,
w)
= "\/" (
{ (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum } ,
(RealPoset [.0,1.])) &
(R (#) (S (#) T)) . (
x,
w)
= "\/" (
{ ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } ,
(RealPoset [.0,1.])) )
by Th22;
hence
((R (#) S) (#) T) . (
x,
w)
= (R (#) (S (#) T)) . (
x,
w)
by A4, A11, A8, TARSKI:2;
verum
end;
thus
(R (#) S) (#) T = R (#) (S (#) T)
by A1; verum