let S, S9 be non empty non void ManySortedSign ; :: thesis:
let A1, A2 be MSAlgebra over 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 S9, the carrier of S; :: thesis:
let g be Function; :: thesis:
assume A3: f,g form_morphism_between S9,S ; :: thesis:
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:
thus h9 = h * f ; :: thesis:
let o be OperSymbol of S9; :: according to MSUALG_3:def 7 :: thesis:
set go = g . o;
assume A6: Args (o,(A1 | (S9,f,g))) <> {} ; :: thesis:
let x be Element of Args (o,(A1 | (S9,f,g))); :: thesis:
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: