X . a is Subset of ( the Sorts of Q . a)
by A1, Th13;

then A4: [x,y] in [:(X . a),( the Sorts of Q . a):] by A3, ZFMISC_1:87;

A5: [|X, the Sorts of Q|] . a = [:(X . a),( the Sorts of Q . a):] by PBOOLE:def 16;

dom [|X, the Sorts of Q|] = the carrier of J by PARTFUN1:def 2;

then A6: [x,y] in Union [|X, the Sorts of Q|] by A4, A5, CARD_5:2;

then A7: ( not the Sorts of Q . j is empty & [A,[x,y]] in [:( the Sorts of Q . j),(Union [|X, the Sorts of Q|]):] ) by A2, ZFMISC_1:87;

dom the Sorts of Q = the carrier of J by PARTFUN1:def 2;

then A8: A in Union the Sorts of Q by A2, CARD_5:2;

then [A,[x,y]] in [:(Union the Sorts of Q),(Union [|X, the Sorts of Q|]):] by A6, ZFMISC_1:87;

then [A,[x,y]] in dom the subst-op of Q by A8, FUNCT_2:def 1;

then ( the subst-op of Q . [A,[x,y]] in the subst-op of Q .: [:( the Sorts of Q . j),(Union [|X, the Sorts of Q|]):] & the subst-op of Q .: [:( the Sorts of Q . j),(Union [|X, the Sorts of Q|]):] c= the Sorts of Q . j ) by Def10, A7, FUNCT_1:def 6;

hence the subst-op of Q . [A,[x,y]] is Element of Q,j ; :: thesis: verum

then A4: [x,y] in [:(X . a),( the Sorts of Q . a):] by A3, ZFMISC_1:87;

A5: [|X, the Sorts of Q|] . a = [:(X . a),( the Sorts of Q . a):] by PBOOLE:def 16;

dom [|X, the Sorts of Q|] = the carrier of J by PARTFUN1:def 2;

then A6: [x,y] in Union [|X, the Sorts of Q|] by A4, A5, CARD_5:2;

then A7: ( not the Sorts of Q . j is empty & [A,[x,y]] in [:( the Sorts of Q . j),(Union [|X, the Sorts of Q|]):] ) by A2, ZFMISC_1:87;

dom the Sorts of Q = the carrier of J by PARTFUN1:def 2;

then A8: A in Union the Sorts of Q by A2, CARD_5:2;

then [A,[x,y]] in [:(Union the Sorts of Q),(Union [|X, the Sorts of Q|]):] by A6, ZFMISC_1:87;

then [A,[x,y]] in dom the subst-op of Q by A8, FUNCT_2:def 1;

then ( the subst-op of Q . [A,[x,y]] in the subst-op of Q .: [:( the Sorts of Q . j),(Union [|X, the Sorts of Q|]):] & the subst-op of Q .: [:( the Sorts of Q . j),(Union [|X, the Sorts of Q|]):] c= the Sorts of Q . j ) by Def10, A7, FUNCT_1:def 6;

hence the subst-op of Q . [A,[x,y]] is Element of Q,j ; :: thesis: verum