thus
( V is trivial implies for a being Element of V holds a = 0. V )
; :: thesis: ( ( for u being Element of V holds u = 0. V ) implies V is trivial )

assume A1: for a being Element of V holds a = 0. V ; :: thesis: V is trivial

let a, b be Element of V; :: according to STRUCT_0:def 10 :: thesis: a = b

thus a = 0. V by A1

.= b by A1 ; :: thesis: verum

assume A1: for a being Element of V holds a = 0. V ; :: thesis: V is trivial

let a, b be Element of V; :: according to STRUCT_0:def 10 :: thesis: a = b

thus a = 0. V by A1

.= b by A1 ; :: thesis: verum