let F be non degenerated right_complementable Abelian add-associative right_zeroed distributive Field-like doubleLoopStr ; :: thesis: for a being Element of F holds
( a * (1. F) = a & (1. F) * a = a )
let a be Element of H₁(F); :: thesis: ( a * (1. F) = a & (1. F) * a = a )

per cases ( a = 0. F or a is Element of NonZero F ) by ZFMISC_1:56;

suppose A1: a = 0. F ; :: thesis: ( a * (1. F) = a & (1. F) * a = a )

hence a * (1. F) = a ; :: thesis: (1. F) * a = a
thus (1. F) * a = a by A1; :: thesis: verum

end;

suppose a is Element of NonZero F ; :: thesis: ( a * (1. F) = a & (1. F) * a = a )

hence ( a * (1. F) = a & (1. F) * a = a ) by Th6; :: thesis: verum

end;

end;