let D be non empty set ; for f being BinOp of D
for x being non empty FinSequence of D
for y being Element of D holds
( (MultPlace f) . <*y*> = y & (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y) )
let f be BinOp of D; for x being non empty FinSequence of D
for y being Element of D holds
( (MultPlace f) . <*y*> = y & (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y) )
set F = MultPlace f;
let x be non empty FinSequence of D; for y being Element of D holds
( (MultPlace f) . <*y*> = y & (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y) )
let y be Element of D; ( (MultPlace f) . <*y*> = y & (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y) )
consider k being Nat such that
A1:
k + 1 = len x
by NAT_1:6;
reconsider x0 = x as Element of (D *) \ {{}} by Th5;
reconsider x1 = x ^ <*y*> as non empty FinSequence of D ;
1 in Seg 1
;
then
1 in dom <*y*>
by FINSEQ_1:def 8;
then A2: x1 . ((len x) + 1) =
<*y*> . 1
by FINSEQ_1:def 7
.=
y
by FINSEQ_1:40
;
A3: x1 | (len x) =
x | (len x)
by FINSEQ_5:22
.=
x
by FINSEQ_3:49
;
A4:
len <*y*> = 1
by FINSEQ_1:40;
then A5:
len x1 = (len x) + 1
by FINSEQ_1:22;
reconsider y1 = <*y*> as non empty FinSequence of D ;
reconsider y2 = y1 as Element of (D *) \ {{}} by Th5;
(len y2) - 1 = 0
by A4;
then (MultPlace f) . y2 =
(MultPlace (f,y2)) . 0
by Def9
.=
y2 . 1
by Def7
.=
y
by FINSEQ_1:def 8
;
hence
(MultPlace f) . <*y*> = y
; (MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y)
reconsider x2 = x1 as Element of (D *) \ {{}} by Th5;
(MultPlace f) . x2 =
(MultPlace (f,x2)) . ((len x2) - 1)
by Def9
.=
f . (((MultPlace (f,x2)) . k),(x2 . (k + 2)))
by Def7, A1, A5
.=
f . (((MultPlace (f,x0)) . ((len x) - 1)),(x2 . ((len x) + 1)))
by A3, A1, Lm14
.=
f . (((MultPlace f) . x0),y)
by A2, Def9
;
hence
(MultPlace f) . (x ^ <*y*>) = f . (((MultPlace f) . x),y)
; verum