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
( Args o2,A = Args o1,(A | S1,f,g) & Result o1,(A | S1,f,g) = Result 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
( Args o2,A = Args o1,(A | S1,f,g) & Result o1,(A | S1,f,g) = Result 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
( Args o2,A = Args o1,(A | S1,f,g) & Result o1,(A | S1,f,g) = Result o2,A )
A2: dom f = the carrier of S1 by A1, PUA2MSS1:def 13;
let A be MSAlgebra of S2; :: thesis: for o1 being OperSymbol of S1
for o2 being OperSymbol of S2 st o2 = g . o1 holds
( Args o2,A = Args o1,(A | S1,f,g) & Result o1,(A | S1,f,g) = Result o2,A )
let o1 be OperSymbol of S1; :: thesis: for o2 being OperSymbol of S2 st o2 = g . o1 holds
( Args o2,A = Args o1,(A | S1,f,g) & Result o1,(A | S1,f,g) = Result o2,A )
let o2 be OperSymbol of S2; :: thesis: ( o2 = g . o1 implies ( Args o2,A = Args o1,(A | S1,f,g) & Result o1,(A | S1,f,g) = Result o2,A ) )
assume A3: o2 = g . o1 ; :: thesis: ( Args o2,A = Args o1,(A | S1,f,g) & Result o1,(A | S1,f,g) = Result o2,A )
thus Args o2,A = product (the Sorts of A * (the_arity_of o2)) by PRALG_2:10
.= product (the Sorts of A * (f * (the_arity_of o1))) by A1, A3, PUA2MSS1:def 13
.= product ((the Sorts of A * f) * (the_arity_of o1)) by RELAT_1:55
.= product (the Sorts of (A | S1,f,g) * (the_arity_of o1)) by A1, Def3
.= Args o1,(A | S1,f,g) by PRALG_2:10 ; :: thesis: Result o1,(A | S1,f,g) = Result o2,A
dom g = the carrier' of S1 by A1, PUA2MSS1:def 13;
then the_result_sort_of o2 = (the ResultSort of S2 * g) . o1 by A3, FUNCT_1:23
.= (f * the ResultSort of S1) . o1 by A1, PUA2MSS1:def 13
.= f . (the_result_sort_of o1) by FUNCT_2:21 ;
hence Result o2,A = the Sorts of A . (f . (the_result_sort_of o1)) by PRALG_2:10
.= (the Sorts of A * f) . (the_result_sort_of o1) by A2, FUNCT_1:23
.= the Sorts of (A | S1,f,g) . (the_result_sort_of o1) by A1, Def3
.= Result o1,(A | S1,f,g) by PRALG_2:10 ;
:: thesis: verum