let D be non empty set ; :: thesis: for d being Element of D
for f being BinOp of D holds
( (MultPlace f) . <*d*> = d & ( for x being D -valued FinSequence st not x is empty holds
(MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ) )
let d be Element of D; :: thesis: for f being BinOp of D holds
( (MultPlace f) . <*d*> = d & ( for x being D -valued FinSequence st not x is empty holds
(MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ) )
let f be BinOp of D; :: thesis: ( (MultPlace f) . <*d*> = d & ( for x being D -valued FinSequence st not x is empty holds
(MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ) )
set F = MultPlace f;
thus (MultPlace f) . <*d*> = d by Lm15; :: thesis: for x being D -valued FinSequence st not x is empty holds
(MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d)
let x be D -valued FinSequence; :: thesis: ( not x is empty implies (MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) )
assume not x is empty ; :: thesis: (MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d)
then reconsider xx = x as non empty FinSequence of D by Lm1;
(MultPlace f) . (xx ^ <*d*>) = f . (((MultPlace f) . xx),d) by Lm15;
hence (MultPlace f) . (x ^ <*d*>) = f . (((MultPlace f) . x),d) ; :: thesis: verum