let i be Nat; :: thesis: for K being non empty addLoopStr
for a1, a2 being Element of K holds (i |-> a1) - (i |-> a2) = i |-> (a1 - a2)
let K be non empty addLoopStr ; :: thesis: for a1, a2 being Element of K holds (i |-> a1) - (i |-> a2) = i |-> (a1 - a2)
let a1, a2 be Element of K; :: thesis: (i |-> a1) - (i |-> a2) = i |-> (a1 - a2)
thus (i |-> a1) - (i |-> a2) = i |-> ((diffield K) . (a1,a2)) by FINSEQOP:17
.= i |-> (a1 - a2) by Th11 ; :: thesis: verum