consider f being Function such that
A1: ( dom f = F₁() & ( for x being object st x in F₁() holds
( ( P₁[x] implies f . x = F₂(x) ) & ( P₁[x] implies f . x = F₃(x) ) ) ) ) from PARTFUN1:sch 1();
take f ; :: thesis: ( dom f = F₁() & ( for x being Element of F₁() holds
( ( P₁[x] implies f . x = F₂(x) ) & ( P₁[x] implies f . x = F₃(x) ) ) ) )
thus ( dom f = F₁() & ( for x being Element of F₁() holds
( ( P₁[x] implies f . x = F₂(x) ) & ( P₁[x] implies f . x = F₃(x) ) ) ) ) by A1; :: thesis: verum