let X be non empty set ; :: thesis: ( dom (canon_image X,1) = X & ( for x being set st x in X holds
(canon_image X,1) . x = [x,1] ) )
dom (canon_image X,1) = free_magma X,1 by FUNCT_2:def 1;
hence dom (canon_image X,1) = X by Def14; :: thesis: for x being set st x in X holds
(canon_image X,1) . x = [x,1]
hence for x being set st x in X holds
(canon_image X,1) . x = [x,1] by Def20; :: thesis: verum