let S1, S2 be non empty ManySortedSign ; for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g))
let f, g be Function; ( f,g form_morphism_between S1,S2 implies for A being MSAlgebra over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g)) )
assume A1:
f,g form_morphism_between S1,S2
; for A being MSAlgebra over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g))
( dom f = the carrier of S1 & rng f c= the carrier of S2 )
by A1;
then reconsider f = f as Function of the carrier of S1, the carrier of S2 by FUNCT_2:def 1, RELSET_1:4;
let A be MSAlgebra over S2; (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g))
hence
(id the Sorts of A) * f = id the Sorts of (A | (S1,f,g))
by PBOOLE:3; verum