let R be non empty left_add-cancelable right_zeroed left-distributive doubleLoopStr ; :: thesis: for I being non empty Subset of R holds (0. R) * I = {(0. R)}
let I be non empty Subset of R; :: thesis: (0. R) * I = {(0. R)}
A1: now :: thesis: for u being object st u in {(0. R)} holds
u in (0. R) * I
set j = the Element of I;
let u be object ; :: thesis: ( u in {(0. R)} implies u in (0. R) * I )
assume u in {(0. R)} ; :: thesis: u in (0. R) * I
then A2: u = 0. R by TARSKI:def 1;
(0. R) * the Element of I = 0. R by BINOM:1;
hence u in (0. R) * I by A2; :: thesis: verum
end;
now :: thesis: for u being object st u in (0. R) * I holds
u in {(0. R)}
let u be object ; :: thesis: ( u in (0. R) * I implies u in {(0. R)} )
assume u in (0. R) * I ; :: thesis: u in {(0. R)}
then ex i being Element of R st
( u = (0. R) * i & i in I ) ;
then u = 0. R by BINOM:1;
hence u in {(0. R)} by TARSKI:def 1; :: thesis: verum
end;
hence (0. R) * I = {(0. R)} by A1, TARSKI:2; :: thesis: verum