let S be non empty non void ManySortedSign ; :: thesis: for A, B, C being non-empty MSAlgebra of S
for F1 being ManySortedFunction of A,B
for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds
for G being ManySortedFunction of B,C st G ** F1 = F2 holds
G is_homomorphism B,C
let A, B, C be non-empty MSAlgebra of S; :: thesis: for F1 being ManySortedFunction of A,B
for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds
for G being ManySortedFunction of B,C st G ** F1 = F2 holds
G is_homomorphism B,C
let F1 be ManySortedFunction of A,B; :: thesis: for F2 being ManySortedFunction of A,C st F1 is_epimorphism A,B & F2 is_homomorphism A,C holds
for G being ManySortedFunction of B,C st G ** F1 = F2 holds
G is_homomorphism B,C
let F2 be ManySortedFunction of A,C; :: thesis: ( F1 is_epimorphism A,B & F2 is_homomorphism A,C implies for G being ManySortedFunction of B,C st G ** F1 = F2 holds
G is_homomorphism B,C )
assume that
A1: F1 is_epimorphism A,B and
A2: F2 is_homomorphism A,C ; :: thesis: for G being ManySortedFunction of B,C st G ** F1 = F2 holds
G is_homomorphism B,C
let G be ManySortedFunction of B,C; :: thesis: ( G ** F1 = F2 implies G is_homomorphism B,C )
assume A3: G ** F1 = F2 ; :: thesis: G is_homomorphism B,C
let o be OperSymbol of S; :: according to MSUALG_3:def 9 :: thesis: ( Args o,B = {} or for b₁ being Element of Args o,B holds (G . (the_result_sort_of o)) . ((Den o,B) . b₁) = (Den o,C) . (G # b₁) )
assume Args o,B <> {} ; :: thesis: for b₁ being Element of Args o,B holds (G . (the_result_sort_of o)) . ((Den o,B) . b₁) = (Den o,C) . (G # b₁)
let x be Element of Args o,B; :: thesis: (G . (the_result_sort_of o)) . ((Den o,B) . x) = (Den o,C) . (G # x)
F1 is "onto" by A1, MSUALG_3:def 10;
then consider y being Element of Args o,A such that
A4: F1 # y = x by Th18;
set r = the_result_sort_of o;
F1 is_homomorphism A,B by A1, MSUALG_3:def 10;
then A5: (F1 . (the_result_sort_of o)) . ((Den o,A) . y) = (Den o,B) . x by A4, MSUALG_3:def 9;
A6: (F2 . (the_result_sort_of o)) . ((Den o,A) . y) = ((G . (the_result_sort_of o)) * (F1 . (the_result_sort_of o))) . ((Den o,A) . y) by A3, MSUALG_3:2
.= (G . (the_result_sort_of o)) . ((Den o,B) . x) by A5, Th19, FUNCT_2:21 ;
(F2 . (the_result_sort_of o)) . ((Den o,A) . y) = (Den o,C) . ((G ** F1) # y) by A2, A3, MSUALG_3:def 9
.= (Den o,C) . (G # x) by A4, MSUALG_3:8 ;
hence (G . (the_result_sort_of o)) . ((Den o,B) . x) = (Den o,C) . (G # x) by A6; :: thesis: verum