let S be non empty non void ManySortedSign ; :: thesis: for A, B, C being non-empty MSAlgebra over 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 over 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 7 :: 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;
then consider y being Element of Args (o,A) such that
A4: F1 # y = x by Th17;
set r = the_result_sort_of o;
F1 is_homomorphism A,B by A1;
then A5: (F1 . (the_result_sort_of o)) . ((Den (o,A)) . y) = (Den (o,B)) . x by A4;
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, Th18, FUNCT_2:15 ;
(F2 . (the_result_sort_of o)) . ((Den (o,A)) . y) = (Den (o,C)) . ((G ** F1) # y) by A2, A3
.= (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