deffunc H_{1}( object , object ) -> set = (id (Union Q)) . J;

A1: for j, y being object st j in Union Q & y in Y holds

H_{1}(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_{1}(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_{1}(a,b) & H_{1}(a,b) = a )
by A2, A3, A4, FUNCT_1:17, CARD_5:2;

hence x in Q . j by A4; :: thesis: verum

A1: for j, y being object st j in Union Q & y in Y holds

H

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

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

hence x in Q . j by A4; :: thesis: verum