consider f being Function such that
A1: ( dom f = F1() & ( for x being object st x in F1() holds
f . x = F2(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 = F2(x) by A1;
hence f . x is Cardinal ; :: thesis: verum
end;
then reconsider f = f as Cardinal-Function ;
take f ; :: thesis: ( dom f = F1() & ( for x being set st x in F1() holds
f . x = F2(x) ) )
thus ( dom f = F1() & ( for x being set st x in F1() holds
f . x = F2(x) ) ) by A1; :: thesis: verum