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