let i be Element of NAT ; :: thesis: for K being non empty addLoopStr
for a1, a2 being Element of K
for p1, p2 being FinSequence of the carrier of K st i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i holds
(p1 - p2) . i = a1 - a2
let K be non empty addLoopStr ; :: thesis: for a1, a2 being Element of K
for p1, p2 being FinSequence of the carrier of K st i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i holds
(p1 - p2) . i = a1 - a2
let a1, a2 be Element of K; :: thesis: for p1, p2 being FinSequence of the carrier of K st i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i holds
(p1 - p2) . i = a1 - a2
let p1, p2 be FinSequence of the carrier of K; :: thesis: ( i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i implies (p1 - p2) . i = a1 - a2 )
assume that
A1: i in dom (p1 - p2) and
A2: ( a1 = p1 . i & a2 = p2 . i ) ; :: thesis: (p1 - p2) . i = a1 - a2
(p1 - p2) . i = (diffield K) . a1,a2 by A1, A2, FUNCOP_1:28;
hence (p1 - p2) . i = a1 - a2 by Th14; :: thesis: verum