let S1, S2 be non empty ManySortedSign ; :: thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra of S2 holds (id the Sorts of A) * f = id the Sorts of (A | S1,f,g)
let f, g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies for A being MSAlgebra of 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 ; :: thesis: for A being MSAlgebra of S2 holds (id the Sorts of A) * f = id the Sorts of (A | S1,f,g)
let A be MSAlgebra of S2; :: thesis: (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, PUA2MSS1:def 13;
then reconsider f = f as Function of the carrier of S1,the carrier of S2 by FUNCT_2:def 1, RELSET_1:11;

now

let i be set ; :: thesis: ( i in the carrier of S1 implies ((id the Sorts of A) * f) . i = (id the Sorts of (A | S1,f,g)) . i )
assume i in the carrier of S1 ; :: thesis: ((id the Sorts of A) * f) . i = (id the Sorts of (A | S1,f,g)) . i
then reconsider s = i as SortSymbol of S1 ;
thus ((id the Sorts of A) * f) . i = (id the Sorts of A) . (f . s) by FUNCT_2:21
.= id (the Sorts of A . (f . s)) by MSUALG_3:def 1
.= id ((the Sorts of A * f) . s) by FUNCT_2:21
.= id (the Sorts of (A | S1,f,g) . s) by A1, Def3
.= (id the Sorts of (A | S1,f,g)) . i by MSUALG_3:def 1 ; :: thesis: verum

end;

hence (id the Sorts of A) * f = id the Sorts of (A | S1,f,g) by PBOOLE:3; :: thesis: verum