let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S
for A being feasible MSAlgebra over 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 over S; :: thesis: for A being feasible MSAlgebra over 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 over 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 7 :: 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, Th18;
set r = the_result_sort_of o;
A5: x in Args (o,A) by A4, Th18;
Result (o,C) <> {} by A4, MSUALG_6:def 1;
then (Den (o,C)) . x in Result (o,C) by A4, FUNCT_2:5;
then A6: (Den (o,C)) . x in the Sorts of C . ( the ResultSort of S . o) by FUNCT_2:15;
(Den (o,A)) . x = (Den (o,C)) . x by A4, Th19;
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:39
.= (Den (o,U0)) . (h # y) by A2, A5
.= (Den (o,U0)) . (g # x) by A1, A3, A4, Th21 ;
:: thesis: verum