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