let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra of S
for U3 being non-empty MSSubAlgebra of U2
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds
F is_homomorphism U1,U2
let U1, U2 be non-empty MSAlgebra of S; :: thesis: for U3 being non-empty MSSubAlgebra of U2
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds
F is_homomorphism U1,U2
let U3 be non-empty MSSubAlgebra of U2; :: thesis: for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds
F is_homomorphism U1,U2
let F be ManySortedFunction of U1,U2; :: thesis: for G being ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds
F is_homomorphism U1,U2
let G be ManySortedFunction of U1,U3; :: thesis: ( F = G & G is_homomorphism U1,U3 implies F is_homomorphism U1,U2 )
assume that
A1: F = G and
A2: G is_homomorphism U1,U3 ; :: thesis: F is_homomorphism U1,U2
for o being OperSymbol of S st Args o,U1 <> {} holds
for x being Element of Args o,U1 holds (F . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U2) . (F # x)

proof

reconsider S3 = the Sorts of U3 as V2() MSSubset of U2 by MSUALG_2:def 10;
let o be OperSymbol of S; :: thesis: ( Args o,U1 <> {} implies for x being Element of Args o,U1 holds (F . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U2) . (F # x) )
assume Args o,U1 <> {} ; :: thesis: for x being Element of Args o,U1 holds (F . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U2) . (F # x)
let x be Element of Args o,U1; :: thesis: (F . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U2) . (F # x)
for i being set st i in the carrier of S holds
G . i is Function of (the Sorts of U1 . i),(the Sorts of U2 . i)

proof

reconsider S3 = the Sorts of U3 as V2() MSSubset of U2 by MSUALG_2:def 10;
let i be set ; :: thesis: ( i in the carrier of S implies G . i is Function of (the Sorts of U1 . i),(the Sorts of U2 . i) )
assume A3: i in the carrier of S ; :: thesis: G . i is Function of (the Sorts of U1 . i),(the Sorts of U2 . i)
then reconsider g = G . i as Function of (the Sorts of U1 . i),(the Sorts of U3 . i) by PBOOLE:def 18;
the Sorts of U3 is MSSubset of U2 by MSUALG_2:def 10;
then the Sorts of U3 c= the Sorts of U2 by PBOOLE:def 23;
then S3 . i c= the Sorts of U2 . i by A3, PBOOLE:def 5;
then g is Function of (the Sorts of U1 . i),(the Sorts of U2 . i) by A3, FUNCT_2:9;
hence G . i is Function of (the Sorts of U1 . i),(the Sorts of U2 . i) ; :: thesis: verum

end;

then reconsider G1 = G as ManySortedFunction of U1,U2 by PBOOLE:def 18;
S3 is opers_closed by MSUALG_2:def 10;
then A4: S3 is_closed_on o by MSUALG_2:def 7;
the Charact of U3 = Opers U2,S3 by MSUALG_2:def 10;
then A5: Den o,U3 = (Opers U2,S3) . o by MSUALG_1:def 11
.= o /. S3 by MSUALG_2:def 9
.= (Den o,U2) | (((S3 # ) * the Arity of S) . o) by A4, MSUALG_2:def 8 ;
A6: dom x = dom (the_arity_of o) by Th6;

A7: now

let a be set ; :: thesis: ( a in dom (the_arity_of o) implies (G # x) . a = (G1 # x) . a )
assume A8: a in dom (the_arity_of o) ; :: thesis: (G # x) . a = (G1 # x) . a
then reconsider n = a as Nat ;
(G # x) . n = (G . ((the_arity_of o) /. n)) . (x . n) by A6, A8, Def8;
hence (G # x) . a = (G1 # x) . a by A6, A8, Def8; :: thesis: verum

end;

( dom (G # x) = dom (the_arity_of o) & dom (G1 # x) = dom (the_arity_of o) ) by Th6;
then A9: G # x = G1 # x by A7, FUNCT_1:9;
dom (Den o,U2) = Args o,U2 by FUNCT_2:def 1;
then A10: ( ((S3 # ) * the Arity of S) . o = Args o,U3 & F # x in (dom (Den o,U2)) /\ (Args o,U3) ) by A1, A9, MSUALG_1:def 9, XBOOLE_0:def 4;
(F . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U3) . (F # x) by A1, A2, A9, Def9;
hence (F . (the_result_sort_of o)) . ((Den o,U1) . x) = (Den o,U2) . (F # x) by A5, A10, FUNCT_1:71; :: thesis: verum

end;

hence F is_homomorphism U1,U2 by Def9; :: thesis: verum