let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra of S
for A being feasible MSAlgebra of S
for C being feasible MSSubAlgebra of A
for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds
for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds
for g being ManySortedFunction of C,U0 st g = h || D holds
g is_homomorphism C,U0
let U0 be non-empty MSAlgebra of S; :: thesis: for A being feasible MSAlgebra of S
for C being feasible MSSubAlgebra of A
for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds
for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds
for g being ManySortedFunction of C,U0 st g = h || D holds
g is_homomorphism C,U0
let A be feasible MSAlgebra of S; :: thesis: for C being feasible MSSubAlgebra of A
for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds
for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds
for g being ManySortedFunction of C,U0 st g = h || D holds
g is_homomorphism C,U0
let C be feasible MSSubAlgebra of A; :: thesis: for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds
for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds
for g being ManySortedFunction of C,U0 st g = h || D holds
g is_homomorphism C,U0
let D be ManySortedSubset of the Sorts of A; :: thesis: ( D = the Sorts of C implies for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds
for g being ManySortedFunction of C,U0 st g = h || D holds
g is_homomorphism C,U0 )
assume A1: D = the Sorts of C ; :: thesis: for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds
for g being ManySortedFunction of C,U0 st g = h || D holds
g is_homomorphism C,U0
let h be ManySortedFunction of A,U0; :: thesis: ( h is_homomorphism A,U0 implies for g being ManySortedFunction of C,U0 st g = h || D holds
g is_homomorphism C,U0 )
assume A2: h is_homomorphism A,U0 ; :: thesis: for g being ManySortedFunction of C,U0 st g = h || D holds
g is_homomorphism C,U0
let g be ManySortedFunction of C,U0; :: thesis: ( g = h || D implies g is_homomorphism C,U0 )
assume A3: g = h || D ; :: thesis: g is_homomorphism C,U0
let o be OperSymbol of S; :: according to MSUALG_3:def 9 :: thesis: ( Args o,C = {} or for b₁ being Element of Args o,C holds (g . (the_result_sort_of o)) . ((Den o,C) . b₁) = (Den o,U0) . (g # b₁) )
assume A4: Args o,C <> {} ; :: thesis: for b₁ being Element of Args o,C holds (g . (the_result_sort_of o)) . ((Den o,C) . b₁) = (Den o,U0) . (g # b₁)
let x be Element of Args o,C; :: thesis: (g . (the_result_sort_of o)) . ((Den o,C) . x) = (Den o,U0) . (g # x)
reconsider y = x as Element of Args o,A by A4, Th20;
set r = the_result_sort_of o;
A5: x in Args o,A by A4, Th20;
Result o,C <> {} by A4, MSUALG_6:def 1;
then (Den o,C) . x in Result o,C by A4, FUNCT_2:7;
then A6: (Den o,C) . x in the Sorts of C . (the ResultSort of S . o) by FUNCT_2:21;
(Den o,A) . x = (Den o,C) . x by A4, Th21;
hence (g . (the_result_sort_of o)) . ((Den o,C) . x) = (h . (the_result_sort_of o)) . ((Den o,A) . x) by A1, A3, A6, INSTALG1:40
.= (Den o,U0) . (h # y) by A2, A5, MSUALG_3:def 9
.= (Den o,U0) . (g # x) by A1, A3, A4, Th23 ;
:: thesis: verum