deffunc H₁( object , object ) -> set = (id (Union Q)) . J;
A1: for j, y being object st j in Union Q & y in Y holds
H₁(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) = H₁(j,y) from BINOP_1:sch 2(A1);
take F ; :: thesis: F is sort-preserving
let j be Element of J; :: according to AOFA_L00:def 10 :: thesis: F .: [:(Q . j),Y:] c= Q . j
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F .: [:(Q . j),Y:] or x in Q . j )
assume x in F .: [:(Q . j),Y:] ; :: thesis: 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) = H₁(a,b) & H₁(a,b) = a ) by A2, A3, A4, FUNCT_1:17, CARD_5:2;
hence x in Q . j by A4; :: thesis: verum