let R be non empty left_unital doubleLoopStr ; :: thesis: for I being Subset of R holds (1. R) * I = I
let I be Subset of R; :: thesis: (1. R) * I = I

A1: now

let u be set ; :: thesis: ( u in I implies u in (1. R) * I )
assume A2: u in I ; :: thesis: u in (1. R) * I
then reconsider u9 = u as Element of R ;
(1. R) * u9 = u9 by VECTSP_1:def 8;
hence u in (1. R) * I by A2; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in (1. R) * I implies u in I )
assume u in (1. R) * I ; :: thesis: u in I
then ex i being Element of R st
( u = (1. R) * i & i in I ) ;
hence u in I by VECTSP_1:def 8; :: thesis: verum

end;

hence (1. R) * I = I by A1, TARSKI:1; :: thesis: verum