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

A4: [|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 A5: [x,t] in Union [|X, the Sorts of Q|] by A3, A4, CARD_5:2;

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

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

then A7: A in Union the Sorts of Q by A1, CARD_5:2;

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

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

then ( the subst-op of Q . [A,[x,t]] 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, A6, FUNCT_1:def 6;

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

A4: [|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 A5: [x,t] in Union [|X, the Sorts of Q|] by A3, A4, CARD_5:2;

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

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

then A7: A in Union the Sorts of Q by A1, CARD_5:2;

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

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

then ( the subst-op of Q . [A,[x,t]] 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, A6, FUNCT_1:def 6;

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