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