A3: for a being object st a in F₃() holds
( ( P₁[a] implies F₄(a) in F₂() ) & ( P₁[a] implies F₅(a) in F₂() ) ) by A1, A2;
consider f being Function of F₃(),F₂() such that
A4: for x being object st x in F₃() holds
( ( P₁[x] implies f . x = F₄(x) ) & ( P₁[x] implies f . x = F₅(x) ) ) from FUNCT_2:sch 5(A3);
take f ; :: thesis: for a being Element of F₁() st a in F₃() holds
( ( P₁[a] implies f . a = F₄(a) ) & ( P₁[a] implies f . a = F₅(a) ) )
thus for a being Element of F₁() st a in F₃() holds
( ( P₁[a] implies f . a = F₄(a) ) & ( P₁[a] implies f . a = F₅(a) ) ) by A4; :: thesis: verum