let K be non empty addLoopStr ; :: thesis: for a1, a2 being Element of K holds <*a1*> - <*a2*> = <*(a1 - a2)*>
let a1, a2 be Element of K; :: thesis: <*a1*> - <*a2*> = <*(a1 - a2)*>
thus <*a1*> - <*a2*> = <*((diffield K) . (a1,a2))*> by FINSEQ_2:74
.= <*(a1 - a2)*> by Th11 ; :: thesis: verum