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:88
.= <*(a1 - a2)*> by Th14 ; :: thesis: verum