let n be Nat; :: thesis: for F being non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr

for A being Matrix of n,F holds A + (0. (F,n)) = A

let F be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for A being Matrix of n,F holds A + (0. (F,n)) = A

let A be Matrix of n,F; :: thesis: A + (0. (F,n)) = A

A1: Indices A = Indices (A + (0. (F,n))) by MATRIX_0:26;

A2: Indices A = Indices (0. (F,n)) by MATRIX_0:26;

for A being Matrix of n,F holds A + (0. (F,n)) = A

let F be non empty right_complementable Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for A being Matrix of n,F holds A + (0. (F,n)) = A

let A be Matrix of n,F; :: thesis: A + (0. (F,n)) = A

A1: Indices A = Indices (A + (0. (F,n))) by MATRIX_0:26;

A2: Indices A = Indices (0. (F,n)) by MATRIX_0:26;

now :: thesis: for i, j being Nat st [i,j] in Indices (A + (0. (F,n))) holds

(A + (0. (F,n))) * (i,j) = A * (i,j)

hence
A + (0. (F,n)) = A
by MATRIX_0:27; :: thesis: verum(A + (0. (F,n))) * (i,j) = A * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in Indices (A + (0. (F,n))) implies (A + (0. (F,n))) * (i,j) = A * (i,j) )

assume A3: [i,j] in Indices (A + (0. (F,n))) ; :: thesis: (A + (0. (F,n))) * (i,j) = A * (i,j)

hence (A + (0. (F,n))) * (i,j) = (A * (i,j)) + ((0. (F,n)) * (i,j)) by A1, Def5

.= (A * (i,j)) + (0. F) by A1, A2, A3, Th1

.= A * (i,j) by RLVECT_1:4 ;

:: thesis: verum

end;assume A3: [i,j] in Indices (A + (0. (F,n))) ; :: thesis: (A + (0. (F,n))) * (i,j) = A * (i,j)

hence (A + (0. (F,n))) * (i,j) = (A * (i,j)) + ((0. (F,n)) * (i,j)) by A1, Def5

.= (A * (i,j)) + (0. F) by A1, A2, A3, Th1

.= A * (i,j) by RLVECT_1:4 ;

:: thesis: verum