consider f being Function such that
A1: ( dom f = F₁() & ( for x being object st x in F₁() holds
f . x = F₂(x) ) ) from FUNCT_1:sch 3();
f is Cardinal-yielding

proof

let x be object ; :: according to CARD_3:def 1 :: thesis: ( x in dom f implies f . x is Cardinal )
assume x in dom f ; :: thesis: f . x is Cardinal
then f . x = F₂(x) by A1;
hence f . x is Cardinal ; :: thesis: verum

end;

then reconsider f = f as Cardinal-Function ;
take f ; :: thesis: ( dom f = F₁() & ( for x being set st x in F₁() holds
f . x = F₂(x) ) )
thus ( dom f = F₁() & ( for x being set st x in F₁() holds
f . x = F₂(x) ) ) by A1; :: thesis: verum