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