deffunc H_{1}( object ) -> object = F_{3}(($1 `1),($1 `2));

consider f being Function such that

A1: dom f = [:F_{1}(),F_{2}():]
and

A2: for x being object st x in [:F_{1}(),F_{2}():] holds

f . x = H_{1}(x)
from FUNCT_1:sch 3();

reconsider f = f as ManySortedSet of [:F_{1}(),F_{2}():] by A1, PARTFUN1:def 2, RELAT_1:def 18;

take f ; :: thesis: for i, j being set st i in F_{1}() & j in F_{2}() holds

f . (i,j) = F_{3}(i,j)

let i, j be set ; :: thesis: ( i in F_{1}() & j in F_{2}() implies f . (i,j) = F_{3}(i,j) )

assume ( i in F_{1}() & j in F_{2}() )
; :: thesis: f . (i,j) = F_{3}(i,j)

then A3: [i,j] in [:F_{1}(),F_{2}():]
by ZFMISC_1:87;

( [i,j] `1 = i & [i,j] `2 = j ) ;

hence f . (i,j) = F_{3}(i,j)
by A2, A3; :: thesis: verum

consider f being Function such that

A1: dom f = [:F

A2: for x being object st x in [:F

f . x = H

reconsider f = f as ManySortedSet of [:F

take f ; :: thesis: for i, j being set st i in F

f . (i,j) = F

let i, j be set ; :: thesis: ( i in F

assume ( i in F

then A3: [i,j] in [:F

( [i,j] `1 = i & [i,j] `2 = j ) ;

hence f . (i,j) = F