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 5;
hence (.: (pr2 (X,Y))) . E = (pr2 (X,Y)) .: E by FUNCT_3:def 1; :: thesis: verum