let K be non empty addLoopStr ; :: thesis: for a1, a2 being Element of K holds (diffield K) . a1,a2 = a1 - a2
let a1, a2 be Element of K; :: thesis: (diffield K) . a1,a2 = a1 - a2
thus (diffield K) . a1,a2 = the addF of K . a1,((comp K) . a2) by FINSEQOP:87
.= a1 - a2 by VECTSP_1:def 25 ; :: thesis: verum