let S, S' be non empty non void ManySortedSign ; :: thesis:
let A1, A2 be MSAlgebra of S; :: thesis:
assume A1: the Sorts of A1 is_transformable_to the Sorts of A2 ; :: thesis:
let h be ManySortedFunction of A1,A2; :: thesis:
assume A2: h is_homomorphism A1,A2 ; :: thesis:
let f be Function of the carrier of S',the carrier of S; :: thesis:
let g be Function; :: thesis:
assume A3: f,g form_morphism_between S',S ; :: thesis:
set B1 = A1 | S',f,g;
set B2 = A2 | S',f,g;
reconsider h' = h * f as ManySortedFunction of (A1 | S',f,g),(A2 | S',f,g) by A3, Th30;
( dom g = the carrier' of S' & rng g c= the carrier' of S ) by A3, PUA2MSS1:def 13;
then reconsider g = g as Function of the carrier' of S',the carrier' of S by FUNCT_2:def 1, RELSET_1:11;
take h' ; :: thesis:
thus h' = h * f ; :: thesis:
let o be OperSymbol of S'; :: according to MSUALG_3:def 9 :: thesis:
assume A4: Args o,(A1 | S',f,g) <> {} ; :: thesis:
A5: ( Args o,(A1 | S',f,g) = Args (g . o),A1 & Args o,(A2 | S',f,g) = Args (g . o),A2 ) by A3, Th25;
then A6: Args o,(A2 | S',f,g) <> {} by A1, A4, Th3;
let x be Element of Args o,(A1 | S',f,g); :: thesis:
set go = g . o;
reconsider y = x as Element of Args (g . o),A1 by A3, Th25;
A7: h' # x = h # y by A3, A4, A5, A6, Th34;
A8: ( Den o,(A1 | S',f,g) = Den (g . o),A1 & Den o,(A2 | S',f,g) = Den (g . o),A2 ) by A3, Th24;
A9: f * the ResultSort of S' = the ResultSort of S * g by A3, PUA2MSS1:def 13;
h' . (the_result_sort_of o) = h . (f . (the_result_sort_of o)) by FUNCT_2:21
.= h . ((the ResultSort of S * g) . o) by A9, FUNCT_2:21
.= h . (the_result_sort_of (g . o)) by FUNCT_2:21 ;
hence (h' . (the_result_sort_of o)) . ((Den o,(A1 | S',f,g)) . x) = (Den o,(A2 | S',f,g)) . (h' # x) by A2, A4, A5, A7, A8, MSUALG_3:def 9; :: thesis: