let i be Element of 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:18
.= i |-> (a1 - a2) by Th14 ; :: thesis: verum