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 ;
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 ;
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 b1 being Element of Args (o,(A1 | (S9,f,g))) holds (h9 . ) . ((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))) <> {} ; :: thesis: for b1 being Element of Args (o,(A1 | (S9,f,g))) holds (h9 . ) . ((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))); :: thesis: (h9 . ) . ((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 ;
A7: h9 . = h . (f . ) by FUNCT_2:15
.= h . (( the ResultSort of S * g) . o) by
.= 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 ;
A9: Args (o,(A1 | (S9,f,g))) = Args ((g . o),A1) by ;
A10: Args (o,(A2 | (S9,f,g))) = Args ((g . o),A2) by ;
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 . ) . ((Den (o,(A1 | (S9,f,g)))) . x) = (Den (o,(A2 | (S9,f,g)))) . (h9 # x) by A2, A6, A9, A8, A7; :: thesis: verum