let S, S9 be non empty non void ManySortedSign ; for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
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
ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )
let A1, A2 be MSAlgebra over S; ( the Sorts of A1 is_transformable_to the Sorts of A2 implies for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
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
ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) )
assume A1:
the Sorts of A1 is_transformable_to the Sorts of A2
; for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
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
ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )
let h be ManySortedFunction of A1,A2; ( h is_homomorphism A1,A2 implies 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
ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) )
assume A2:
h is_homomorphism A1,A2
; 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
ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )
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
ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )
let g be Function; ( f,g form_morphism_between S9,S implies ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) ) )
assume A3:
f,g form_morphism_between S9,S
; ex h9 being ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) st
( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )
A4:
( dom g = the carrier' of S9 & rng g c= the carrier' of S )
by A3;
set B1 = A1 | (S9,f,g);
set B2 = A2 | (S9,f,g);
reconsider g = g as Function of the carrier' of S9, the carrier' of S by A4, FUNCT_2:def 1, RELSET_1:4;
A5:
f * the ResultSort of S9 = the ResultSort of S * g
by A3;
reconsider h9 = h * f as ManySortedFunction of (A1 | (S9,f,g)),(A2 | (S9,f,g)) by A3, Th29;
take
h9
; ( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )
thus
h9 = h * f
; h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g)
let o be OperSymbol of S9; MSUALG_3:def 7 ( Args (o,(A1 | (S9,f,g))) = {} or for b1 being Element of Args (o,(A1 | (S9,f,g))) holds (h9 . (the_result_sort_of o)) . ((Den (o,(A1 | (S9,f,g)))) . b1) = (Den (o,(A2 | (S9,f,g)))) . (h9 # b1) )
set go = g . o;
assume A6:
Args (o,(A1 | (S9,f,g))) <> {}
; for b1 being Element of Args (o,(A1 | (S9,f,g))) holds (h9 . (the_result_sort_of o)) . ((Den (o,(A1 | (S9,f,g)))) . b1) = (Den (o,(A2 | (S9,f,g)))) . (h9 # b1)
let x be Element of Args (o,(A1 | (S9,f,g))); (h9 . (the_result_sort_of o)) . ((Den (o,(A1 | (S9,f,g)))) . x) = (Den (o,(A2 | (S9,f,g)))) . (h9 # x)
reconsider y = x as Element of Args ((g . o),A1) by A3, Th24;
A7: h9 . (the_result_sort_of o) =
h . (f . (the_result_sort_of o))
by FUNCT_2:15
.=
h . (( the ResultSort of S * g) . o)
by A5, FUNCT_2:15
.=
h . (the_result_sort_of (g . o))
by FUNCT_2:15
;
A8:
( Den (o,(A1 | (S9,f,g))) = Den ((g . o),A1) & Den (o,(A2 | (S9,f,g))) = Den ((g . o),A2) )
by A3, Th23;
A9:
Args (o,(A1 | (S9,f,g))) = Args ((g . o),A1)
by A3, Th24;
A10:
Args (o,(A2 | (S9,f,g))) = Args ((g . o),A2)
by A3, Th24;
then
Args (o,(A2 | (S9,f,g))) <> {}
by A1, A6, A9, Th2;
then
h9 # x = h # y
by A3, A6, A9, A10, Th33;
hence
(h9 . (the_result_sort_of o)) . ((Den (o,(A1 | (S9,f,g)))) . x) = (Den (o,(A2 | (S9,f,g)))) . (h9 # x)
by A2, A6, A9, A8, A7; verum