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
( 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 over 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 over 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;
let A be MSAlgebra over 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:3
.= product ( the Sorts of A * (f * (the_arity_of o1))) by A1, A3
.= product (( the Sorts of A * f) * (the_arity_of o1)) by RELAT_1:36
.= product ( the Sorts of (A | (S1,f,g)) * (the_arity_of o1)) by A1, Def3
.= Args (o1,(A | (S1,f,g))) by PRALG_2:3 ; :: thesis: Result (o1,(A | (S1,f,g))) = Result (o2,A)
dom g = the carrier' of S1 by A1;
then the_result_sort_of o2 = ( the ResultSort of S2 * g) . o1 by A3, FUNCT_1:13
.= (f * the ResultSort of S1) . o1 by A1
.= f . (the_result_sort_of o1) by FUNCT_2:15 ;
hence Result (o2,A) = the Sorts of A . (f . (the_result_sort_of o1)) by PRALG_2:3
.= ( the Sorts of A * f) . (the_result_sort_of o1) by A2, FUNCT_1:13
.= the Sorts of (A | (S1,f,g)) . (the_result_sort_of o1) by A1, Def3
.= Result (o1,(A | (S1,f,g))) by PRALG_2:3 ;
:: thesis: verum