let h1, h2 be ManySortedFunction of (Free (S,X)),A1; :: thesis: ( h1 is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = h1 || G ) & h2 is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = h2 || G ) implies h1 = h2 )
assume that
A3: ( h1 is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = h1 || G ) ) and
A4: ( h2 is_homomorphism Free (S,X),A1 & ( for G being GeneratorSet of Free (S,X) st G = FreeGen X holds
id G = h2 || G ) ) ; :: thesis: h1 = h2
reconsider H = FreeGen X as V5() GeneratorSet of Free (S,X) by MSAFREE3:31;
h1 || H = id H by A3
.= h2 || H by A4 ;
hence h1 = h2 by A3, A4, EXTENS_1:19; :: thesis: verum