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