defpred S1[ set , set ] means ( P1[\$1] & P2[\$2] );
A2: for x being Element of F2()
for y being Element of F3() holds
( S1[x,y] iff S1[x,y] ) ;
A3: for x being Element of F2()
for y being Element of F3() st S1[x,y] holds
F4(x,y) = F5(x,y) by A1;
A4: { F4(x9,y9) where x9 is Element of F2(), y9 is Element of F3() : S1[x9,y9] } = { F5(x,y) where x is Element of F2(), y is Element of F3() : S1[x,y] } from A5: "\/" ( { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } ,F1()) = "\/" ( { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ,F1()) from "\/" ( { ("\/" ( { F5(x9,y9) where x9 is Element of F2() : P1[x9] } ,F1())) where y9 is Element of F3() : P2[y9] } ,F1()) = "\/" ( { F5(x9,y9) where x9 is Element of F2(), y9 is Element of F3() : ( P1[x9] & P2[y9] ) } ,F1()) from
.= "\/" ( { F4(x9,y9) where x9 is Element of F2(), y9 is Element of F3() : ( P1[x9] & P2[y9] ) } ,F1()) by A4 ;
hence "\/" ( { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } ,F1()) = "\/" ( { ("\/" ( { F5(x9,y9) where x9 is Element of F2() : P1[x9] } ,F1())) where y9 is Element of F3() : P2[y9] } ,F1()) by A5; :: thesis: verum