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