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 over 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 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 ; :: thesis: 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; :: thesis: (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g))

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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g))

now :: thesis: for i being object st i in the carrier of S1 holds

((id the Sorts of A) * f) . i = (id the Sorts of (A | (S1,f,g))) . i

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

let i be object ; :: 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:15

.= id ( the Sorts of A . (f . s)) by MSUALG_3:def 1

.= id (( the Sorts of A * f) . s) by FUNCT_2:15

.= 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;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:15

.= id ( the Sorts of A . (f . s)) by MSUALG_3:def 1

.= id (( the Sorts of A * f) . s) by FUNCT_2:15

.= 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