consider f being Function such that
A2: ( dom f = F₁() & rng f c= F₂() ) and
A3: for x being object st x in F₁() holds
P₁[x,f . x] from FUNCT_1:sch 6(A1);
reconsider f = f as Function of F₁(),F₂() by A2, Th2;
take f ; :: thesis: for x being object st x in F₁() holds
P₁[x,f . x]
thus for x being object st x in F₁() holds
P₁[x,f . x] by A3; :: thesis: verum