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 A1: 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]
thus for x being set st x in X holds
(canon_image X,1) . x = [x,1] by A1, Def20; :: thesis: verum