let R be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for i being Integer holds i '*' (0. R) = 0. R
let i be Integer; :: thesis: i '*' (0. R) = 0. R
defpred S₁[ Integer] means $1 '*' (0. R) = 0. R;
A2: S₁[ 0 ] by RING_3:59;
A3: for u being Integer st S₁[u] holds
( S₁[u - 1] & S₁[u + 1] )

proof

let u be Integer; :: thesis: ( S₁[u] implies ( S₁[u - 1] & S₁[u + 1] ) )
assume A4: S₁[u] ; :: thesis: ( S₁[u - 1] & S₁[u + 1] )
set a = 0. R;

now :: thesis: for k being Integer st k = u - 1 holds
k '*' (0. R) = 0. R

let k be Integer; :: thesis: ( k = u - 1 implies k '*' (0. R) = 0. R )
assume k = u - 1 ; :: thesis: k '*' (0. R) = 0. R
hence k '*' (0. R) = (u '*' (0. R)) - (1 '*' (0. R)) by RING_3:64
.= (0. R) - (0. R) by A4, RING_3:60
.= 0. R ;
:: thesis: verum

end;

hence S₁[u - 1] ; :: thesis: S₁[u + 1]

now :: thesis: for k being Integer st k = u + 1 holds
k '*' (0. R) = 0. R

let k be Integer; :: thesis: ( k = u + 1 implies k '*' (0. R) = 0. R )
assume k = u + 1 ; :: thesis: k '*' (0. R) = 0. R
hence k '*' (0. R) = (u '*' (0. R)) + (1 '*' (0. R)) by RING_3:62
.= 0. R by A4, RING_3:60 ;
:: thesis: verum

end;

hence S₁[u + 1] ; :: thesis: verum

end;

for i being Integer holds S₁[i] from INT_1:sch 4(A2, A3);
hence i '*' (0. R) = 0. R ; :: thesis: verum