let L be non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr ; :: thesis: ( 0. L = 1. L implies L is trivial )
assume A1: 0. L = 1. L ; :: thesis: L is trivial
let u be Element of L; :: according to STRUCT_0:def 19 :: thesis: u = 0. L
thus u = u * (0. L) by A1, VECTSP_1:def 13
.= 0. L by VECTSP_1:36 ; :: thesis: verum