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 of 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 of 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 of 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 Th10;
let A be MSAlgebra of 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:21
.= the Charact of (A | S1,f,g) . o1 by A1, Def3 ;
hence Den o1,(A | S1,f,g) = Den o2,A ; :: thesis: verum