A2: now :: thesis: for x being Element of F₁() holds F₃(x) in F₂()

let x be Element of F₁(); :: thesis: F₃(x) in F₂()
F₃(x) is Element of F₂() by A1;
hence F₃(x) in F₂() ; :: thesis: verum

end;

consider f being Function of F₁(),F₂() such that
A3: for x being Element of F₁() holds f . x = F₃(x) from FUNCT_2:sch 8(A2);
take f ; :: thesis: for x being Element of F₁() holds f . x = F₃(x)
thus for x being Element of F₁() holds f . x = F₃(x) by A3; :: thesis: verum