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 :: thesis: for u being object st u in I holds
u in (1. R) * I

let u be object ; :: 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 ;
hence u in (1. R) * I by A2; :: thesis: verum

end;

now :: thesis: for u being object st u in (1. R) * I holds
u in I

let u be object ; :: 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 ; :: thesis: verum

end;

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