let D be non empty set ; :: thesis: for f being BinOp of D st f is associative holds
for d being Element of D
for m being Nat
for x being Element of (m + 1) -tuples_on D holds (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x))
let f be BinOp of D; :: thesis: ( f is associative implies for d being Element of D
for m being Nat
for x being Element of (m + 1) -tuples_on D holds (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x)) )
set F = MultPlace f;
assume A1: f is associative ; :: thesis: for d being Element of D
for m being Nat
for x being Element of (m + 1) -tuples_on D holds (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x))
let d be Element of D; :: thesis: for m being Nat
for x being Element of (m + 1) -tuples_on D holds (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x))
defpred S₁[ Nat] means for x being Element of ($1 + 1) -tuples_on D holds (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x));
A2: S₁[ 0 ]

proof

let x be Element of (0 + 1) -tuples_on D; :: thesis: (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x))
consider xx being Element of D such that
A3: x = <*xx*> by FINSEQ_2:97;
(MultPlace f) . (<*d*> ^ x) = f . (((MultPlace f) . <*d*>),xx) by Lm15, A3
.= f . (d,xx) by Lm15
.= f . (d,((MultPlace f) . x)) by Lm15, A3 ;
hence (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x)) ; :: thesis: verum

end;

A4: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A5: S₁[m] ; :: thesis: S₁[m + 1]
let x be Element of ((m + 1) + 1) -tuples_on D; :: thesis: (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x))
( (m + 1) + 0 <= (m + 1) + 1 & len x = (m + 1) + 1 ) by CARD_1:def 7, XREAL_1:8;
then len (x | (m + 1)) = m + 1 by FINSEQ_1:59;
then reconsider xx = x | (m + 1) as Element of (m + 1) -tuples_on D by FINSEQ_2:92;
reconsider xxx = xx as non empty FinSequence of D ;
reconsider y = x /. (len x) as Element of D ;
reconsider XX = (MultPlace f) . xxx as Element of D by FUNCT_2:5, Th5;
A6: (m + 1) + 1 = len x by CARD_1:def 7;
then (MultPlace f) . (<*d*> ^ x) = (MultPlace f) . (<*d*> ^ ((x | (m + 1)) ^ <*y*>)) by FINSEQ_5:21
.= (MultPlace f) . ((<*d*> ^ xx) ^ <*y*>) by FINSEQ_1:32
.= f . (((MultPlace f) . (<*d*> ^ xx)),y) by Lm15
.= f . ((f . (d,((MultPlace f) . xx))),y) by A5
.= f . (d,(f . (XX,y))) by A1
.= f . (d,((MultPlace f) . (xxx ^ <*y*>))) by Lm15
.= f . (d,((MultPlace f) . x)) by FINSEQ_5:21, A6 ;
hence (MultPlace f) . (<*d*> ^ x) = f . (d,((MultPlace f) . x)) ; :: thesis: verum

end;

thus for m being Nat holds S₁[m] from NAT_1:sch 2(A2, A4); :: thesis: verum