let S be non empty non void ManySortedSign ; :: thesis: for o being OperSymbol of S
for A1 being non-empty disjoint_valued MSAlgebra of S
for A2 being non-empty MSAlgebra of 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 of S
for A2 being non-empty MSAlgebra of 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 of S; :: thesis: for A2 being non-empty MSAlgebra of 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 of 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:23;
then A2: a in product (the Sorts of A1 * (the_arity_of o)) by PBOOLE:def 19;
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:45, ZFMISC_1:95;
then rng a c= union (rng the Sorts of A1) by XBOOLE_1:1;
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:46;
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 4;
then A5: dom (the Sorts of A1 * (the_arity_of o)) = dom (the_arity_of o) by A4, RELAT_1:46;
A6: dom a = dom (the Sorts of A1 * (the_arity_of o)) by A2, CARD_3:18;

A7: now

let x be set ; :: 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:44;
then A10: the Sorts of A2 . ((the_arity_of o) . x) = (the Sorts of A2 * (the_arity_of o)) . x by A8, FUNCT_1:23;
(the_arity_of o) . x in rng (the_arity_of o) by A9, A8, FUNCT_1:def 5;
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:23;
then A11: a . x in the Sorts of A1 . z by A2, A5, A9, A8, CARD_3:18;
((Flatten f) * a) . x = (Flatten f) . (a . x) by A6, A5, A9, A8, FUNCT_1:23
.= (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:7; :: thesis: verum

end;

dom the Sorts of A2 = the carrier of S by PARTFUN1:def 4;
then dom (the_arity_of o) = dom (the Sorts of A2 * (the_arity_of o)) by A4, RELAT_1:46;
then (Flatten f) * a in product (the Sorts of A2 * (the_arity_of o)) by A3, A6, A5, A7, CARD_3:18;
then (Flatten f) * a in (the Sorts of A2 # ) . (the Arity of S . o) by PBOOLE:def 19;
then reconsider x = (Flatten f) * a as Element of Args o,A2 by A1, FUNCT_1:23;

now

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:18, PARTFUN1:def 8;
then A13: a . n in the Sorts of A1 . ((the_arity_of o) /. n) by A6, A5, A12, FUNCT_1:23;
thus x . n = (Flatten f) . (a . n) by A12, FUNCT_1:23
.= (f . ((the_arity_of o) /. n)) . (a . n) by A13, Def1 ; :: thesis: verum

end;

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