let S be non empty non void ManySortedSign ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: for a being Element of Args (o,A1) holds (Flatten f) * a = f # a
let a be Element of Args (o,A1); :: thesis: (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 :: thesis: 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)) . x

let x be object ; :: thesis: ( 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)) ; :: thesis: ((Flatten f) * a) . x in ( the Sorts of A2 * (the_arity_of o)) . x
A9: 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; :: thesis: 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;

now :: thesis: for n being Nat st n in dom a holds
x . n = (f . ((the_arity_of o) /. n)) . (a . n)

let n be Nat; :: thesis: ( n in dom a implies x . n = (f . ((the_arity_of o) /. n)) . (a . n) )
assume A12: n in dom a ; :: thesis: x . n = (f . ((the_arity_of o) /. n)) . (a . n)
then ( (the_arity_of o) /. n = (the_arity_of o) . n & a . n in ( the Sorts of A1 * (the_arity_of o)) . n ) by A2, A6, A5, CARD_3:9, PARTFUN1:def 6;
then A13: a . n in the Sorts of A1 . ((the_arity_of o) /. n) by A6, A5, A12, FUNCT_1:13;
thus x . n = (Flatten f) . (a . n) by A12, FUNCT_1:13
.= (f . ((the_arity_of o) /. n)) . (a . n) by A13, Def1 ; :: thesis: verum

end;

hence (Flatten f) * a = f # a by MSUALG_3:def 6; :: thesis: verum