[|X, the Sorts of T|] . a = [:(X . a),( the Sorts of T . a):] by PBOOLE:def 16;
then ( dom [|X, the Sorts of T|] = the carrier of J & [x,t] in [|X, the Sorts of T|] . a ) by ZFMISC_1:87, PARTFUN1:def 2;
hence the assignments of A . [x,t] is Algorithm of A by CARD_5:2, FUNCT_2:5; :: thesis: verum