reconsider f9 = (canon_image Y,1) * f as Function of X,(free_magma Y) by Th39;
ex h being Function of (free_magma X),(free_magma Y) st
( h is multiplicative & h extends f9 * ((canon_image X,1) " ) ) by Th40;
hence ex b₁ being Function of (free_magma X),(free_magma Y) st
( b₁ is multiplicative & b₁ extends ((canon_image Y,1) * f) * ((canon_image X,1) " ) ) ; :: thesis: verum