let S be non empty non void ManySortedSign ; 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; 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; 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; 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; ( 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
; 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 9;
let o be
OperSymbol of
S;
( 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)
<> {}
;
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);
(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)
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;
(
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;
verum
end;
hence
F is_homomorphism U1,U2
; verum