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 H1(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;