defpred S_{1}[ set , set ] means ( P_{1}[$1] & P_{2}[$2] );

A2: for x being Element of F_{2}()

for y being Element of F_{3}() holds

( S_{1}[x,y] iff S_{1}[x,y] )
;

A3: for x being Element of F_{2}()

for y being Element of F_{3}() st S_{1}[x,y] holds

F_{4}(x,y) = F_{5}(x,y)
by A1;

A4: { F_{4}(x9,y9) where x9 is Element of F_{2}(), y9 is Element of F_{3}() : S_{1}[x9,y9] } = { F_{5}(x,y) where x is Element of F_{2}(), y is Element of F_{3}() : S_{1}[x,y] }
from LFUZZY_0:sch 4(A2, A3);

A5: "\/" ( { ("\/" ( { F_{4}(x,y) where y is Element of F_{3}() : P_{2}[y] } ,F_{1}())) where x is Element of F_{2}() : P_{1}[x] } ,F_{1}()) = "\/" ( { F_{4}(x,y) where x is Element of F_{2}(), y is Element of F_{3}() : ( P_{1}[x] & P_{2}[y] ) } ,F_{1}())
from LFUZZY_0:sch 1();

"\/" ( { ("\/" ( { F_{5}(x9,y9) where x9 is Element of F_{2}() : P_{1}[x9] } ,F_{1}())) where y9 is Element of F_{3}() : P_{2}[y9] } ,F_{1}()) =
"\/" ( { F_{5}(x9,y9) where x9 is Element of F_{2}(), y9 is Element of F_{3}() : ( P_{1}[x9] & P_{2}[y9] ) } ,F_{1}())
from LFUZZY_0:sch 2()

.= "\/" ( { F_{4}(x9,y9) where x9 is Element of F_{2}(), y9 is Element of F_{3}() : ( P_{1}[x9] & P_{2}[y9] ) } ,F_{1}())
by A4
;

hence "\/" ( { ("\/" ( { F_{4}(x,y) where y is Element of F_{3}() : P_{2}[y] } ,F_{1}())) where x is Element of F_{2}() : P_{1}[x] } ,F_{1}()) = "\/" ( { ("\/" ( { F_{5}(x9,y9) where x9 is Element of F_{2}() : P_{1}[x9] } ,F_{1}())) where y9 is Element of F_{3}() : P_{2}[y9] } ,F_{1}())
by A5; :: thesis: verum

A2: for x being Element of F

for y being Element of F

( S

A3: for x being Element of F

for y being Element of F

F

A4: { F

A5: "\/" ( { ("\/" ( { F

"\/" ( { ("\/" ( { F

.= "\/" ( { F

hence "\/" ( { ("\/" ( { F