let S be non empty non void ManySortedSign ; :: thesis: for U1, U2 being non-empty MSAlgebra over 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 over 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 non-empty MSSubset of U2 by MSUALG_2:def 9;
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 object 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 non-empty MSSubset of U2 by MSUALG_2:def 9;
let i be object ; :: 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 15;
the Sorts of U3 is MSSubset of U2 by MSUALG_2:def 9;
then the Sorts of U3 c= the Sorts of U2 by PBOOLE:def 18;
then S3 . i c= the Sorts of U2 . i by A3, PBOOLE:def 2;
then g is Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by A3, FUNCT_2:7;
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 15;
S3 is opers_closed by MSUALG_2:def 9;
then A4: S3 is_closed_on o ;
the Charact of U3 = Opers (U2,S3) by MSUALG_2:def 9;
then A5: Den (o,U3) = (Opers (U2,S3)) . o by MSUALG_1:def 6
.= o /. S3 by MSUALG_2:def 8
.= (Den (o,U2)) | (((S3 #) * the Arity of S) . o) by A4, MSUALG_2:def 7 ;
A6: dom x = dom (the_arity_of o) by Th6;

A7: now :: thesis: for a being object st a in dom (the_arity_of o) holds
(G # x) . a = (G1 # x) . a

let a be object ; :: 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, Def6;
hence (G # x) . a = (G1 # x) . a by A6, A8, Def6; :: 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:2;
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 4, XBOOLE_0:def 4;
(F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . (F # x) by A1, A2, A9;
hence (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) by A5, A10, FUNCT_1:48; :: thesis: verum

end;

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