set f = F5(); thus
F5() .: { F4(x) where x is Element of F1() : P1[x] } c= { (F5() . F4(x)) where x is Element of F2() : P1[x] } :: according to XBOOLE_0:def 10:: thesis: { (F5() . F4(x)) where x is Element of F2() : P1[x] } c= F5() .: { F4(x) where x is Element of F1() : P1[x] }
let y be object ; :: according to TARSKI:def 3:: thesis: ( not y in F5() .: { F4(x) where x is Element of F1() : P1[x] } or y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } ) assume
y in F5() .: { F4(x) where x is Element of F1() : P1[x] }
; :: thesis: y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } then consider z being object such that
z indom F5()
and A3:
z in { F4(x) where x is Element of F1() : P1[x] } and A4:
y = F5() . z
byFUNCT_1:def 6; consider x being Element of F1() such that A5:
z = F4(x)
and A6:
P1[x]
byA3; reconsider x = x as Element of F2() byA2;
y = F5() . F4(x)
byA4, A5; hence
y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } byA6; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3:: thesis: ( not y in { (F5() . F4(x)) where x is Element of F2() : P1[x] } or y in F5() .: { F4(x) where x is Element of F1() : P1[x] } ) assume
y in { (F5() . F4(x)) where x is Element of F2() : P1[x] }
; :: thesis: y in F5() .: { F4(x) where x is Element of F1() : P1[x] } then consider x being Element of F2() such that A7:
y = F5() . F4(x)
and A8:
P1[x]
; reconsider x = x as Element of F1() byA2; A9:
F4(x) in the carrier of F3()
;
F4(x) in { F4(z) where z is Element of F1() : P1[z] } byA8; hence
y in F5() .: { F4(x) where x is Element of F1() : P1[x] } byA1, A7, A9, FUNCT_1:def 6; :: thesis: verum