A2: now :: thesis: for x being Element of F1() holds F3(x) in F2()
let x be Element of F1(); :: thesis: F3(x) in F2()
F3(x) is Element of F2() by A1;
hence F3(x) in F2() ; :: thesis: verum
end;
consider f being Function of F1(),F2() such that
A3: for x being Element of F1() holds f . x = F3(x) from FUNCT_2:sch 8(A2);
 take f ; :: thesis: for x being Element of F1() holds f . x = F3(x)
thus for x being Element of F1() holds f . x = F3(x) by A3; :: thesis: verum