let e, X, Y be set ; :: thesis: ( e c= [:X,Y:] implies (.: (pr2 (X,Y))) . e = (pr2 (X,Y)) .: e )
assume e c= [:X,Y:] ; :: thesis: (.: (pr2 (X,Y))) . e = (pr2 (X,Y)) .: e
then e c= dom (pr2 (X,Y)) by FUNCT_3:def 6;
hence (.: (pr2 (X,Y))) . e = (pr2 (X,Y)) .: e by FUNCT_3:def 1; :: thesis: verum