deffunc H1( object , object ) -> set = (id (Union Q)) . J;
A1:
for j, y being object st j in Union Q & y in Y holds
H1(j,y) in Union Q
by FUNCT_1:17;
consider F being Function of [:(Union Q),Y:],(Union Q) such that
A2:
for j, y being object st j in Union Q & y in Y holds
F . (j,y) = H1(j,y)
from BINOP_1:sch 2(A1);
take
F
; F is sort-preserving
let j be Element of J; AOFA_L00:def 10 F .: [:(Q . j),Y:] c= Q . j
let x be object ; TARSKI:def 3 ( not x in F .: [:(Q . j),Y:] or x in Q . j )
assume
x in F .: [:(Q . j),Y:]
; x in Q . j
then consider y being object such that
A3:
( y in dom F & y in [:(Q . j),Y:] & x = F . y )
by FUNCT_1:def 6;
consider a, b being object such that
A4:
( a in Q . j & b in Y & y = [a,b] )
by A3, ZFMISC_1:def 2;
dom Q = J
by PARTFUN1:def 2;
then
( x = F . (a,b) & F . (a,b) = H1(a,b) & H1(a,b) = a )
by A2, A3, A4, FUNCT_1:17, CARD_5:2;
hence
x in Q . j
by A4; verum