let S1, S2 be non empty non void ManySortedSign ; 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; ( 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
; 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; 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; 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; ( 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
; ( 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
; 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
;
verum