let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for v being Element of V holds
( Sum <*(0. V),v*> = v & Sum <*v,(0. V)*> = v )
let v be Element of V; :: thesis: ( Sum <*(0. V),v*> = v & Sum <*v,(0. V)*> = v )
thus Sum <*(0. V),v*> = (0. V) + v by Th62
.= v by Th10 ; :: thesis: Sum <*v,(0. V)*> = v
thus Sum <*v,(0. V)*> = v + (0. V) by Th62
.= v by Th10 ; :: thesis: verum