reconsider f9 = (canon_image (Y,1)) * f as Function of X,(free_magma Y) by Th38;
ex h being Function of (free_magma X),(free_magma Y) st
( h is multiplicative & h extends f9 * ((canon_image (X,1)) ") ) by Th39;
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