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