let S be non empty non void ManySortedSign ; for o being OperSymbol of S
for A1 being non-empty disjoint_valued MSAlgebra over S
for A2 being non-empty MSAlgebra over S
for f being ManySortedFunction of A1,A2
for a being Element of Args (o,A1) holds (Flatten f) * a = f # a
let o be OperSymbol of S; for A1 being non-empty disjoint_valued MSAlgebra over S
for A2 being non-empty MSAlgebra over S
for f being ManySortedFunction of A1,A2
for a being Element of Args (o,A1) holds (Flatten f) * a = f # a
let A1 be non-empty disjoint_valued MSAlgebra over S; for A2 being non-empty MSAlgebra over S
for f being ManySortedFunction of A1,A2
for a being Element of Args (o,A1) holds (Flatten f) * a = f # a
let A2 be non-empty MSAlgebra over S; for f being ManySortedFunction of A1,A2
for a being Element of Args (o,A1) holds (Flatten f) * a = f # a
let f be ManySortedFunction of A1,A2; for a being Element of Args (o,A1) holds (Flatten f) * a = f # a
let a be Element of Args (o,A1); (Flatten f) * a = f # a
A1:
dom the Arity of S = the carrier' of S
by FUNCT_2:def 1;
set s = the_arity_of o;
a in (( the Sorts of A1 #) * the Arity of S) . o
;
then
a in ( the Sorts of A1 #) . ( the Arity of S . o)
by A1, FUNCT_1:13;
then A2:
a in product ( the Sorts of A1 * (the_arity_of o))
by FINSEQ_2:def 5;
then
rng a c= Union ( the Sorts of A1 * (the_arity_of o))
by Th1;
then
( union (rng ( the Sorts of A1 * (the_arity_of o))) c= union (rng the Sorts of A1) & rng a c= union (rng ( the Sorts of A1 * (the_arity_of o))) )
by CARD_3:def 4, RELAT_1:26, ZFMISC_1:77;
then
rng a c= union (rng the Sorts of A1)
;
then
rng a c= Union the Sorts of A1
by CARD_3:def 4;
then
rng a c= dom (Flatten f)
by FUNCT_2:def 1;
then A3:
dom ((Flatten f) * a) = dom a
by RELAT_1:27;
A4:
rng (the_arity_of o) c= the carrier of S
by FINSEQ_1:def 4;
dom the Sorts of A1 = the carrier of S
by PARTFUN1:def 2;
then A5:
dom ( the Sorts of A1 * (the_arity_of o)) = dom (the_arity_of o)
by A4, RELAT_1:27;
A6:
dom a = dom ( the Sorts of A1 * (the_arity_of o))
by A2, CARD_3:9;
A7:
now for x being object st x in dom ( the Sorts of A2 * (the_arity_of o)) holds
((Flatten f) * a) . x in ( the Sorts of A2 * (the_arity_of o)) . xlet x be
object ;
( x in dom ( the Sorts of A2 * (the_arity_of o)) implies ((Flatten f) * a) . x in ( the Sorts of A2 * (the_arity_of o)) . x )assume A8:
x in dom ( the Sorts of A2 * (the_arity_of o))
;
((Flatten f) * a) . x in ( the Sorts of A2 * (the_arity_of o)) . xA9:
dom ( the Sorts of A2 * (the_arity_of o)) c= dom (the_arity_of o)
by RELAT_1:25;
then A10:
the
Sorts of
A2 . ((the_arity_of o) . x) = ( the Sorts of A2 * (the_arity_of o)) . x
by A8, FUNCT_1:13;
(the_arity_of o) . x in rng (the_arity_of o)
by A9, A8, FUNCT_1:def 3;
then reconsider z =
(the_arity_of o) . x as
SortSymbol of
S by A4;
the
Sorts of
A1 . ((the_arity_of o) . x) = ( the Sorts of A1 * (the_arity_of o)) . x
by A9, A8, FUNCT_1:13;
then A11:
a . x in the
Sorts of
A1 . z
by A2, A5, A9, A8, CARD_3:9;
((Flatten f) * a) . x =
(Flatten f) . (a . x)
by A6, A5, A9, A8, FUNCT_1:13
.=
(f . z) . (a . x)
by A11, Def1
;
hence
((Flatten f) * a) . x in ( the Sorts of A2 * (the_arity_of o)) . x
by A10, A11, FUNCT_2:5;
verum end;
dom the Sorts of A2 = the carrier of S
by PARTFUN1:def 2;
then
dom (the_arity_of o) = dom ( the Sorts of A2 * (the_arity_of o))
by A4, RELAT_1:27;
then
(Flatten f) * a in product ( the Sorts of A2 * (the_arity_of o))
by A3, A6, A5, A7, CARD_3:9;
then
(Flatten f) * a in ( the Sorts of A2 #) . ( the Arity of S . o)
by FINSEQ_2:def 5;
then reconsider x = (Flatten f) * a as Element of Args (o,A2) by A1, FUNCT_1:13;
hence
(Flatten f) * a = f # a
by MSUALG_3:def 6; verum