consider f being Function such that
A1: ( dom f = F1() & ( for d being set st d in F1() holds
f . d = F2(d) ) ) from FUNCT_1:sch 3();
 take f ; :: thesis: ( dom f = F1() & ( for d being Element of F1() holds f . d = F2(d) ) )
thus ( dom f = F1() & ( for d being Element of F1() holds f . d = F2(d) ) ) by A1; :: thesis: verum