let S, S9 be non empty non void ManySortedSign ; for A being non-empty MSAlgebra over S
for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
let A be non-empty MSAlgebra over S; for f being Function of the carrier of S9, the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
let f be Function of the carrier of S9, the carrier of S; for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
let g be Function; ( f,g form_morphism_between S9,S implies for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2 )
assume A1:
f,g form_morphism_between S9,S
; for B being non-empty MSAlgebra over S9 st B = A | (S9,f,g) holds
for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
A2:
( dom g = the carrier' of S9 & rng g c= the carrier' of S )
by A1;
let B be non-empty MSAlgebra over S9; ( B = A | (S9,f,g) implies for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2 )
assume A3:
B = A | (S9,f,g)
; for s1, s2 being SortSymbol of S9
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
reconsider g = g as Function of the carrier' of S9, the carrier' of S by A2, FUNCT_2:def 1, RELSET_1:4;
let s1, s2 be SortSymbol of S9; for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2
let t be Function; ( t is_e.translation_of B,s1,s2 implies t is_e.translation_of A,f . s1,f . s2 )
given o being OperSymbol of S9 such that A4:
the_result_sort_of o = s2
and
A5:
ex i being Element of NAT st
( i in dom (the_arity_of o) & (the_arity_of o) /. i = s1 & ex a being Function st
( a in Args (o,B) & t = transl (o,i,a,B) ) )
; MSUALG_6:def 5 t is_e.translation_of A,f . s1,f . s2
A6:
f * (the_arity_of o) = the_arity_of (g . o)
by A1;
take
g . o
; MSUALG_6:def 5 ( the_result_sort_of (g . o) = f . s2 & ex b1 being Element of NAT st
( b1 in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. b1 = f . s1 & ex b2 being set st
( b2 in Args ((g . o),A) & t = transl ((g . o),b1,b2,A) ) ) )
f * the ResultSort of S9 = the ResultSort of S * g
by A1;
hence the_result_sort_of (g . o) =
(f * the ResultSort of S9) . o
by FUNCT_2:15
.=
f . s2
by A4, FUNCT_2:15
;
ex b1 being Element of NAT st
( b1 in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. b1 = f . s1 & ex b2 being set st
( b2 in Args ((g . o),A) & t = transl ((g . o),b1,b2,A) ) )
consider i being Element of NAT , a being Function such that
A7:
i in dom (the_arity_of o)
and
A8:
(the_arity_of o) /. i = s1
and
A9:
a in Args (o,B)
and
A10:
t = transl (o,i,a,B)
by A5;
take
i
; ( i in dom (the_arity_of (g . o)) & (the_arity_of (g . o)) /. i = f . s1 & ex b1 being set st
( b1 in Args ((g . o),A) & t = transl ((g . o),i,b1,A) ) )
( rng (the_arity_of o) c= the carrier of S9 & dom f = the carrier of S9 )
by FINSEQ_1:def 4, FUNCT_2:def 1;
hence
i in dom (the_arity_of (g . o))
by A7, A6, RELAT_1:27; ( (the_arity_of (g . o)) /. i = f . s1 & ex b1 being set st
( b1 in Args ((g . o),A) & t = transl ((g . o),i,b1,A) ) )
hence A11: (the_arity_of (g . o)) /. i =
(the_arity_of (g . o)) . i
by PARTFUN1:def 6
.=
f . ((the_arity_of o) . i)
by A7, A6, FUNCT_1:13
.=
f . s1
by A7, A8, PARTFUN1:def 6
;
ex b1 being set st
( b1 in Args ((g . o),A) & t = transl ((g . o),i,b1,A) )
then A12:
dom (transl ((g . o),i,a,A)) = the Sorts of A . (f . s1)
by MSUALG_6:def 4;
A13:
the Sorts of B = the Sorts of A * f
by A1, A3, Def3;
then A14:
the Sorts of B . s1 = the Sorts of A . (f . s1)
by FUNCT_2:15;
A15:
now for x being object st x in the Sorts of B . s1 holds
t . x = (transl ((g . o),i,a,A)) . xlet x be
object ;
( x in the Sorts of B . s1 implies t . x = (transl ((g . o),i,a,A)) . x )assume
x in the
Sorts of
B . s1
;
t . x = (transl ((g . o),i,a,A)) . xthen
(
t . x = (Den (o,B)) . (a +* (i,x)) &
(transl ((g . o),i,a,A)) . x = (Den ((g . o),A)) . (a +* (i,x)) )
by A8, A10, A11, A14, MSUALG_6:def 4;
hence
t . x = (transl ((g . o),i,a,A)) . x
by A1, A3, Th23;
verum end;
take
a
; ( a in Args ((g . o),A) & t = transl ((g . o),i,a,A) )
thus
a in Args ((g . o),A)
by A1, A3, A9, Th24; t = transl ((g . o),i,a,A)
dom t = the Sorts of B . s1
by A8, A10, MSUALG_6:def 4;
hence
t = transl ((g . o),i,a,A)
by A12, A13, A15, FUNCT_2:15; verum