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