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
; verum