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 Def13; :: 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 Def19; :: thesis: verum