defpred S₁[ set , set ] means ( P₁[$1] & P₂[$2] );
A2: for x being Element of F₂()
for y being Element of F₃() holds
( S₁[x,y] iff S₁[x,y] ) ;
A3: for x being Element of F₂()
for y being Element of F₃() st S₁[x,y] holds
F₄(x,y) = F₅(x,y) by A1;
A4: { F₄(x',y') where x' is Element of F₂(), y' is Element of F₃() : S₁[x',y'] } = { F₅(x,y) where x is Element of F₂(), y is Element of F₃() : S₁[x,y] } from LFUZZY_0:sch 4(A2, A3);
A5: "\/" { ("\/" { F₄(x,y) where y is Element of F₃() : P₂[y] } ,F₁()) where x is Element of F₂() : P₁[x] } ,F₁() = "\/" { F₄(x,y) where x is Element of F₂(), y is Element of F₃() : ( P₁[x] & P₂[y] ) } ,F₁() from LFUZZY_0:sch 1();
"\/" { ("\/" { F₅(x',y') where x' is Element of F₂() : P₁[x'] } ,F₁()) where y' is Element of F₃() : P₂[y'] } ,F₁() = "\/" { F₅(x',y') where x' is Element of F₂(), y' is Element of F₃() : ( P₁[x'] & P₂[y'] ) } ,F₁() from LFUZZY_0:sch 2()
.= "\/" { F₄(x',y') where x' is Element of F₂(), y' is Element of F₃() : ( P₁[x'] & P₂[y'] ) } ,F₁() by A4 ;
hence "\/" { ("\/" { F₄(x,y) where y is Element of F₃() : P₂[y] } ,F₁()) where x is Element of F₂() : P₁[x] } ,F₁() = "\/" { ("\/" { F₅(x',y') where x' is Element of F₂() : P₁[x'] } ,F₁()) where y' is Element of F₃() : P₂[y'] } ,F₁() by A5; :: thesis: verum