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:82
.= a1 - a2 by VECTSP_1:def 13 ; :: thesis: verum