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

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