let F be Field; :: thesis: for a being Element of NonZero F
for b, c being Element of the carrier of F st a * b = a * c holds
b = c
let a be Element of NonZero F; :: thesis: for b, c being Element of the carrier 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 by Th25
.= (omf F) . (1. F),b
.= (x * ra) * b by Def18
.= ra * (x * c) by A1, Th23
.= (x * ra) * c by Th23
.= (omf F) . (1. F),c by Def18
.= (1. F) * c
.= c by Th25 ;
hence b = c ; :: thesis: verum