thus ( V is trivial implies for a being Element of V holds a = 0. V ) by STRUCT_0:def 10; :: 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

now

let a, b be Element of V; :: thesis: a = b
thus a = 0. V by A1
.= b by A1 ; :: thesis: verum

end;

hence V is trivial by STRUCT_0:def 10; :: thesis: verum