A2:
( [t1,t2] in [:( the Sorts of T . a),( the Sorts of T . a):] & [:( the Sorts of T . a),( the Sorts of T . a):] = [| the Sorts of T, the Sorts of T|] . a )
by A1, ZFMISC_1:87, PBOOLE:def 16;

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

then [t1,t2] in Union [| the Sorts of T, the Sorts of T|] by A2, CARD_5:2;

hence the equality of L . (t1,t2) is Formula of L by FUNCT_2:5; :: thesis: verum

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

then [t1,t2] in Union [| the Sorts of T, the Sorts of T|] by A2, CARD_5:2;

hence the equality of L . (t1,t2) is Formula of L by FUNCT_2:5; :: thesis: verum