thus ( IT is well-unital implies 1. IT is_a_unity_wrt the multF of IT ) :: thesis: ( 1. IT is_a_unity_wrt the multF of IT implies IT is well-unital )

proof

assume A1: IT is well-unital ; :: thesis: 1. IT is_a_unity_wrt the multF of IT
thus 1. IT is_a_left_unity_wrt the multF of IT :: according to BINOP_1:def 7 :: thesis: 1. IT is_a_right_unity_wrt the multF of IT

proof

let a be Element of IT; :: according to BINOP_1:def 16 :: thesis: the multF of IT . ((1. IT),a) = a
thus the multF of IT . ((1. IT),a) = (1. IT) * a
.= a by A1 ; :: thesis: verum

end;

let a be Element of IT; :: according to BINOP_1:def 17 :: thesis: the multF of IT . (a,(1. IT)) = a
thus the multF of IT . (a,(1. IT)) = a * (1. IT)
.= a by A1 ; :: thesis: verum

end;

assume A2: 1. IT is_a_unity_wrt the multF of IT ; :: thesis: IT is well-unital
let x be Element of IT; :: according to VECTSP_1:def 6 :: thesis: ( x [*] (1. IT) = x & (1. IT) [*] x = x )
1. IT is_a_right_unity_wrt the multF of IT by A2;
hence x * (1. IT) = x ; :: thesis: (1. IT) [*] x = x
1. IT is_a_left_unity_wrt the multF of IT by A2;
hence (1. IT) [*] x = x ; :: thesis: verum