let F be Field; :: thesis: for x being Element of F holds x = (comp F) . ((comp F) . x)
let x be Element of F; :: thesis: x = (comp F) . ((comp F) . x)
thus x = - (- x)
.= (comp F) . (- x) by VECTSP_1:def 13
.= (comp F) . ((comp F) . x) by VECTSP_1:def 13 ; :: thesis: verum