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

consider f being Function such that

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

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

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

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

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

f . (i,j,k) = F_{4}(i,j,k)

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

A3: ( [[i,j],k] `2 = k & [i,j,k] = [[i,j],k] ) ;

A4: ([[i,j],k] `1) `2 = j ;

A5: ([[i,j],k] `1) `1 = i ;

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

then A6: [i,j,k] in [:F_{1}(),F_{2}(),F_{3}():]
by MCART_1:69;

thus f . (i,j,k) = f . [i,j,k] by MULTOP_1:def 1

.= F_{4}(i,j,k)
by A2, A6, A5, A4, 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, k being set st i in F

f . (i,j,k) = F

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

A3: ( [[i,j],k] `2 = k & [i,j,k] = [[i,j],k] ) ;

A4: ([[i,j],k] `1) `2 = j ;

A5: ([[i,j],k] `1) `1 = i ;

assume ( i in F

then A6: [i,j,k] in [:F

thus f . (i,j,k) = f . [i,j,k] by MULTOP_1:def 1

.= F