let F be Field; :: thesis: for a being Element of NonZero F
for b, c being Element of F st a * b = a * c holds
b = c
let a be Element of NonZero F; :: thesis: for b, c being Element of F st a * b = a * c holds
b = c
let b, c be Element of H₁(F); :: thesis: ( a * b = a * c implies b = c )
reconsider x = a as Element of F ;
assume A1: a * b = a * c ; :: thesis: b = c
reconsider ra = (revf F) . a as Element of F by XBOOLE_0:def 5;
b = (1. F) * b
.= (omf F) . ((1. F),b)
.= (x * ra) * b by Def6
.= ra * (x * c) by A1, Th19
.= (x * ra) * c by Th19
.= (omf F) . ((1. F),c) by Def6
.= (1. F) * c
.= c ;
hence b = c ; :: thesis: verum