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