let f1, f2 be Function of (free_magma X),(free_magma Y); :: thesis: ( f1 is multiplicative & f1 extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") & f2 is multiplicative & f2 extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") implies f1 = f2 )
assume A1: ( f1 is multiplicative & f1 extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") ) ; :: thesis: ( not f2 is multiplicative or not f2 extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") or f1 = f2 )
assume A2: ( f2 is multiplicative & f2 extends ((canon_image (Y,1)) * f) * ((canon_image (X,1)) ") ) ; :: thesis: f1 = f2
reconsider f9 = (canon_image (Y,1)) * f as Function of X,(free_magma Y) by Th38;
( f1 extends f9 * ((canon_image (X,1)) ") & f2 extends f9 * ((canon_image (X,1)) ") ) by A1, A2;
hence f1 = f2 by A1, A2, Th40; :: thesis: verum