let i be 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 ( i in dom (p1 - p2) & a1 = p1 . i & a2 = p2 . i ) ; :: thesis: (p1 - p2) . i = a1 - a2
then (p1 - p2) . i = (diffield K) . (a1,a2) by FUNCOP_1:22;
hence (p1 - p2) . i = a1 - a2 by Th11; :: thesis: verum