let n be Nat; :: thesis: for X being non empty addLoopStr
for seq being sequence of X holds (- seq) . n = - (seq . n)
let X be non empty addLoopStr ; :: thesis: for seq being sequence of X holds (- seq) . n = - (seq . n)
let seq be sequence of X; :: thesis: (- seq) . n = - (seq . n)
A1: dom (- seq) = NAT by FUNCT_2:def 1;
A2: dom seq = NAT by FUNCT_2:def 1;
A3: n in NAT by ORDINAL1:def 12;
hence (- seq) . n = (- seq) /. n by PARTFUN1:def 6, A1
.= - (seq /. n) by A1, VFUNCT_1:def 5, A3
.= - (seq . n) by A3, PARTFUN1:def 6, A2 ;
:: thesis: verum