consider f being Function such that

A1: ( dom f = F_{2}() & ( for x being object st x in F_{2}() holds

f . x = F_{3}(x) ) )
from FUNCT_1:sch 3();

{ F_{3}(w) where w is Element of F_{1}() : ( w in F_{2}() & P_{1}[w] ) } c= rng f
_{3}(w) where w is Element of F_{1}() : ( w in F_{2}() & P_{1}[w] ) } c= card F_{2}()
by A1, CARD_1:12; :: thesis: verum

A1: ( dom f = F

f . x = F

{ F

proof

hence
card { F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F_{3}(w) where w is Element of F_{1}() : ( w in F_{2}() & P_{1}[w] ) } or x in rng f )

assume x in { F_{3}(w) where w is Element of F_{1}() : ( w in F_{2}() & P_{1}[w] ) }
; :: thesis: x in rng f

then consider w being Element of F_{1}() such that

A2: x = F_{3}(w)
and

A3: w in F_{2}()
and

P_{1}[w]
;

f . w = x by A1, A2, A3;

hence x in rng f by A1, A3, FUNCT_1:def 3; :: thesis: verum

end;assume x in { F

then consider w being Element of F

A2: x = F

A3: w in F

P

f . w = x by A1, A2, A3;

hence x in rng f by A1, A3, FUNCT_1:def 3; :: thesis: verum