let R be non empty right_complementable Abelian add-associative right_zeroed distributive left_unital doubleLoopStr ; :: thesis: for i, j being Integer holds (i * j) '*' (1. R) = (i '*' (1. R)) * (j '*' (1. R))
let i, j be Integer; :: thesis: (i * j) '*' (1. R) = (i '*' (1. R)) * (j '*' (1. R))
defpred S₁[ Integer] means for k being Integer st k = $1 holds
(k * j) '*' (1. R) = (k '*' (1. R)) * (j '*' (1. R));

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

let k be Integer; :: thesis: ( k = 0 implies (k * j) '*' (1. R) = (k '*' (1. R)) * (j '*' (1. R)) )
assume A1: k = 0 ; :: thesis: (k * j) '*' (1. R) = (k '*' (1. R)) * (j '*' (1. R))
hence (k * j) '*' (1. R) = (0. R) * (j '*' (1. R)) by Th58
.= (k '*' (1. R)) * (j '*' (1. R)) by A1, Th58 ;
:: thesis: verum

end;

then A2: S₁[ 0 ] ;
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] )

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

let k be Integer; :: thesis: ( k = u - 1 implies (k * j) '*' (1. R) = (k '*' (1. R)) * (j '*' (1. R)) )
assume A5: k = u - 1 ; :: thesis: (k * j) '*' (1. R) = (k '*' (1. R)) * (j '*' (1. R))
hence (k * j) '*' (1. R) = ((u * j) - j) '*' (1. R)
.= ((u * j) '*' (1. R)) - (j '*' (1. R)) by Th63
.= ((u '*' (1. R)) * (j '*' (1. R))) - (j '*' (1. R)) by A4
.= ((u '*' (1. R)) * (j '*' (1. R))) + (- ((1. R) * (j '*' (1. R))))
.= ((u '*' (1. R)) * (j '*' (1. R))) + ((- (1. R)) * (j '*' (1. R))) by VECTSP_1:9
.= ((u '*' (1. R)) + (- (1. R))) * (j '*' (1. R)) by VECTSP_1:def 3
.= ((u '*' (1. R)) - (1 '*' (1. R))) * (j '*' (1. R)) by Th59
.= (k '*' (1. R)) * (j '*' (1. R)) by Th63, A5 ;
:: thesis: verum

end;

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

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

let k be Integer; :: thesis: ( k = u + 1 implies (k * j) '*' (1. R) = (k '*' (1. R)) * (j '*' (1. R)) )
assume A6: k = u + 1 ; :: thesis: (k * j) '*' (1. R) = (k '*' (1. R)) * (j '*' (1. R))
hence (k * j) '*' (1. R) = ((u * j) + j) '*' (1. R)
.= ((u * j) '*' (1. R)) + (j '*' (1. R)) by Th61
.= ((u '*' (1. R)) * (j '*' (1. R))) + (j '*' (1. R)) by A4
.= ((u '*' (1. R)) * (j '*' (1. R))) + ((1. R) * (j '*' (1. R)))
.= ((u '*' (1. R)) + (1. R)) * (j '*' (1. R)) by VECTSP_1:def 3
.= ((u '*' (1. R)) + (1 '*' (1. R))) * (j '*' (1. R)) by Th59
.= (k '*' (1. R)) * (j '*' (1. R)) by Th61, A6 ;
:: 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 * j) '*' (1. R) = (i '*' (1. R)) * (j '*' (1. R)) ; :: thesis: verum