deffunc H₁( object ) -> object = F₃(($1 `1),($1 `2));
consider f being Function such that
A1: dom f = [:F₁(),F₂():] and
A2: for x being object st x in [:F₁(),F₂():] holds
f . x = H₁(x) from FUNCT_1:sch 3();
reconsider f = f as ManySortedSet of [:F₁(),F₂():] by A1, PARTFUN1:def 2, RELAT_1:def 18;
take f ; :: thesis: for i, j being set st i in F₁() & j in F₂() holds
f . (i,j) = F₃(i,j)
let i, j be set ; :: thesis: ( i in F₁() & j in F₂() implies f . (i,j) = F₃(i,j) )
assume ( i in F₁() & j in F₂() ) ; :: thesis: f . (i,j) = F₃(i,j)
then A3: [i,j] in [:F₁(),F₂():] by ZFMISC_1:87;
( [i,j] `1 = i & [i,j] `2 = j ) ;
hence f . (i,j) = F₃(i,j) by A2, A3; :: thesis: verum