set f = F4(); thus
F4() .: { F3(x) where x is Element of F1() : P1[x] } c= { (F4() . F3(x)) where x is Element of F1() : P1[x] } :: according to XBOOLE_0:def 10:: thesis: { (F4() . F3(x)) where x is Element of F1() : P1[x] } c= F4() .: { F3(x) where x is Element of F1() : P1[x] }
let y be object ; :: according to TARSKI:def 3:: thesis: ( not y in F4() .: { F3(x) where x is Element of F1() : P1[x] } or y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } ) assume
y in F4() .: { F3(x) where x is Element of F1() : P1[x] }
; :: thesis: y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } then consider z being object such that
z indom F4()
and A2:
z in { F3(x) where x is Element of F1() : P1[x] } and A3:
y = F4() . z
byFUNCT_1:def 6;
ex x being Element of F1() st ( z = F3(x) & P1[x] )
byA2; hence
y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } byA3; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3:: thesis: ( not y in { (F4() . F3(x)) where x is Element of F1() : P1[x] } or y in F4() .: { F3(x) where x is Element of F1() : P1[x] } ) assume
y in { (F4() . F3(x)) where x is Element of F1() : P1[x] }
; :: thesis: y in F4() .: { F3(x) where x is Element of F1() : P1[x] } then consider x being Element of F1() such that A4:
y = F4() . F3(x)
and A5:
P1[x]
; A6:
F3(x) indom F4()
byA1;
F3(x) in { F3(z) where z is Element of F1() : P1[z] } byA5; hence
y in F4() .: { F3(x) where x is Element of F1() : P1[x] } byA4, A6, FUNCT_1:def 6; :: thesis: verum