let S1, S2 be non empty non void ManySortedSign ; :: thesis: for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
Den (o1,(A | (S1,f,g))) = Den (o2,A)
let f, g be Function; :: thesis: ( f,g form_morphism_between S1,S2 implies for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
Den (o1,(A | (S1,f,g))) = Den (o2,A) )
assume A1: f,g form_morphism_between S1,S2 ; :: thesis: for A being MSAlgebra over S2
for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
Den (o1,(A | (S1,f,g))) = Den (o2,A)
then reconsider g9 = g as Function of the carrier' of S1, the carrier' of S2 by Th9;
let A be MSAlgebra over S2; :: thesis: for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
Den (o1,(A | (S1,f,g))) = Den (o2,A)
let o1 be OperSymbol of S1; :: thesis: for o2 being OperSymbol of S2 st o2 = g . o1 holds
Den (o1,(A | (S1,f,g))) = Den (o2,A)
let o2 be OperSymbol of S2; :: thesis: ( o2 = g . o1 implies Den (o1,(A | (S1,f,g))) = Den (o2,A) )
assume o2 = g . o1 ; :: thesis: Den (o1,(A | (S1,f,g))) = Den (o2,A)
then the Charact of A . o2 = ( the Charact of A * g9) . o1 by FUNCT_2:15
.= the Charact of (A | (S1,f,g)) . o1 by A1, Def3 ;
hence Den (o1,(A | (S1,f,g))) = Den (o2,A) ; :: thesis: verum