let S, S9 be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )

thus h9 = h * f ; :: thesis: h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g)

let o be OperSymbol of S9; :: according to MSUALG_3:def 7 :: thesis: ( Args (o,(A1 | (S9,f,g))) = {} or for b_{1} being Element of Args (o,(A1 | (S9,f,g))) holds (h9 . (the_result_sort_of o)) . ((Den (o,(A1 | (S9,f,g)))) . b_{1}) = (Den (o,(A2 | (S9,f,g)))) . (h9 # b_{1}) )

set go = g . o;

assume A6: Args (o,(A1 | (S9,f,g))) <> {} ; :: thesis: for b_{1} being Element of Args (o,(A1 | (S9,f,g))) holds (h9 . (the_result_sort_of o)) . ((Den (o,(A1 | (S9,f,g)))) . b_{1}) = (Den (o,(A2 | (S9,f,g)))) . (h9 # b_{1})

let x be Element of Args (o,(A1 | (S9,f,g))); :: thesis: (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; :: thesis: verum

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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( h9 = h * f & h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g) )

thus h9 = h * f ; :: thesis: h9 is_homomorphism A1 | (S9,f,g),A2 | (S9,f,g)

let o be OperSymbol of S9; :: according to MSUALG_3:def 7 :: thesis: ( Args (o,(A1 | (S9,f,g))) = {} or for b

set go = g . o;

assume A6: Args (o,(A1 | (S9,f,g))) <> {} ; :: thesis: for b

let x be Element of Args (o,(A1 | (S9,f,g))); :: thesis: (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; :: thesis: verum