let L be non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr ; :: thesis: for z being FinSequence of the carrier of L
for i being Nat st not i in dom z holds
LagIPoly (z,i) = Product (rpoly (((len z) |-> 1),z))
let z be FinSequence of the carrier of L; :: thesis: for i being Nat st not i in dom z holds
LagIPoly (z,i) = Product (rpoly (((len z) |-> 1),z))
let i be Nat; :: thesis: ( not i in dom z implies LagIPoly (z,i) = Product (rpoly (((len z) |-> 1),z)) )
assume not i in dom z ; :: thesis: LagIPoly (z,i) = Product (rpoly (((len z) |-> 1),z))
then Del (z,i) = z by WSIERP_1:def 1;
hence LagIPoly (z,i) = Product (rpoly (((len z) |-> 1),z)) ; :: thesis: verum