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