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