A1: for x being set st x in F₁() holds
F₃(x) in F₂() ;
consider IT being Function of F₁(),F₂() such that
A2: for x being set st x in F₁() holds
IT . x = F₃(x) from FUNCT_2:sch 2(A1);
take IT ; :: thesis: for x being set st x in F₁() holds
IT /. x = F₃(x)
let x be set ; :: thesis: ( x in F₁() implies IT /. x = F₃(x) )
assume A3: x in F₁() ; :: thesis: IT /. x = F₃(x)
hence F₃(x) = IT . x by A2
.= IT /. x by A3, FUNCT_2:def 14 ;
:: thesis: verum