let R be Ring; :: thesis: for I, K, i, k, i2 being Nat st [i2,k] in Indices (canMat (i,k,I,K,R)) holds
( ( i2 = i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((1. (R,K)),k) ) & ( i2 <> i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k) ) )
let I, K, i, k, i2 be Nat; :: thesis: ( [i2,k] in Indices (canMat (i,k,I,K,R)) implies ( ( i2 = i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((1. (R,K)),k) ) & ( i2 <> i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k) ) ) )
assume A1: [i2,k] in Indices (canMat (i,k,I,K,R)) ; :: thesis: ( ( i2 = i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((1. (R,K)),k) ) & ( i2 <> i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k) ) )
then [i2,k] in [:(dom (canMat (i,k,I,K,R))),(Seg (width (canMat (i,k,I,K,R)))):] by MATRIX_0:def 4;
then A2: i2 in dom (canMat (i,k,I,K,R)) by ZFMISC_1:87;
set p = Line ((canMat (i,k,I,K,R)),i2);
A3: dom (Line ((canMat (i,k,I,K,R)),i2)) = Seg (len (Line ((canMat (i,k,I,K,R)),i2))) by FINSEQ_1:def 3
.= Seg (width (canMat (i,k,I,K,R))) by MATRIX_0:def 7 ;
A4: for k9 being Nat st k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) holds
[i2,k9] in Indices (canMat (i,k,I,K,R))

proof

let k9 be Nat; :: thesis: ( k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) implies [i2,k9] in Indices (canMat (i,k,I,K,R)) )
assume k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) ; :: thesis: [i2,k9] in Indices (canMat (i,k,I,K,R))
then [i2,k9] in [:(dom (canMat (i,k,I,K,R))),(Seg (width (canMat (i,k,I,K,R)))):] by A2, A3, ZFMISC_1:87;
hence [i2,k9] in Indices (canMat (i,k,I,K,R)) by MATRIX_0:def 4; :: thesis: verum

end;

per cases ( ( I <> 0 & i in dom (canMat (i,k,I,K,R)) ) or I = 0 or ( I <> 0 & not i in dom (canMat (i,k,I,K,R)) ) ) ;

suppose A5: ( I <> 0 & i in dom (canMat (i,k,I,K,R)) ) ; :: thesis: ( ( i2 = i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((1. (R,K)),k) ) & ( i2 <> i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k) ) )

then A6: dom (Line ((canMat (i,k,I,K,R)),i2)) = Seg K by A3, Th43;
A7: for k9 being Nat st k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) holds
[i,k9] in Indices (canMat (i,k,I,K,R))

proof

let k9 be Nat; :: thesis: ( k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) implies [i,k9] in Indices (canMat (i,k,I,K,R)) )
assume k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) ; :: thesis: [i,k9] in Indices (canMat (i,k,I,K,R))
then [i,k9] in [:(dom (canMat (i,k,I,K,R))),(Seg (width (canMat (i,k,I,K,R)))):] by A5, A3, ZFMISC_1:87;
hence [i,k9] in Indices (canMat (i,k,I,K,R)) by MATRIX_0:def 4; :: thesis: verum

end;

[i2,k] in [:(dom (canMat (i,k,I,K,R))),(Seg (width (canMat (i,k,I,K,R)))):] by A1, MATRIX_0:def 4;
then k in Seg (width (canMat (i,k,I,K,R))) by ZFMISC_1:87;
then A8: k in Seg K by A5, Th43;
thus ( i2 = i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((1. (R,K)),k) ) :: thesis: ( i2 <> i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k) )

proof

assume A9: i2 = i ; :: thesis: Line ((canMat (i,k,I,K,R)),i2) = Line ((1. (R,K)),k)
set q = Line ((1. (R,K)),k);
A10: dom (Line ((1. (R,K)),k)) = Seg (len (Line ((1. (R,K)),k))) by FINSEQ_1:def 3
.= Seg (width (1. (R,K))) by MATRIX_0:def 7
.= Seg K by MATRIX_0:24 ;
for k9 being Nat st k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) holds
(Line ((canMat (i,k,I,K,R)),i2)) . k9 = (Line ((1. (R,K)),k)) . k9

proof

let k9 be Nat; :: thesis: ( k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) implies (Line ((canMat (i,k,I,K,R)),i2)) . k9 = (Line ((1. (R,K)),k)) . k9 )
assume A11: k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) ; :: thesis: (Line ((canMat (i,k,I,K,R)),i2)) . k9 = (Line ((1. (R,K)),k)) . k9
then A12: [i,k9] in Indices (canMat (i,k,I,K,R)) by A7;
k9 in Seg (len (Line ((1. (R,K)),k))) by A6, A10, A11, FINSEQ_1:def 3;
then A13: k9 in Seg (width (1. (R,K))) by MATRIX_0:def 7;
[k,k9] in [:(Seg K),(Seg K):] by A6, A8, A11, ZFMISC_1:87;
then A14: [k,k9] in Indices (1. (R,K)) by MATRIX_0:24;

per cases ( k9 = k or k9 <> k ) ;

suppose A15: k9 = k ; :: thesis: (Line ((canMat (i,k,I,K,R)),i2)) . k9 = (Line ((1. (R,K)),k)) . k9

thus (Line ((canMat (i,k,I,K,R)),i2)) . k9 = (canMat (i,k,I,K,R)) * (i,k9) by A3, A9, A11, MATRIX_0:def 7
.= 1. R by A15, A12, Th40
.= (1. (R,K)) * (k,k) by A14, A15, MATRIX_1:def 3
.= (Line ((1. (R,K)),k)) . k9 by A13, A15, MATRIX_0:def 7 ; :: thesis: verum

end;

suppose A16: k9 <> k ; :: thesis: (Line ((canMat (i,k,I,K,R)),i2)) . k9 = (Line ((1. (R,K)),k)) . k9

thus (Line ((canMat (i,k,I,K,R)),i2)) . k9 = (canMat (i,k,I,K,R)) * (i,k9) by A3, A9, A11, MATRIX_0:def 7
.= 0. R by A16, A12, Th40
.= (1. (R,K)) * (k,k9) by A14, A16, MATRIX_1:def 3
.= (Line ((1. (R,K)),k)) . k9 by A13, MATRIX_0:def 7 ; :: thesis: verum

end;

end;

end;

hence Line ((canMat (i,k,I,K,R)),i2) = Line ((1. (R,K)),k) by A6, A10, FINSEQ_1:13; :: thesis: verum

end;

assume A17: i2 <> i ; :: thesis: Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k)
set q = Line ((0. (R,K)),k);
A18: dom (Line ((0. (R,K)),k)) = Seg (len (Line ((0. (R,K)),k))) by FINSEQ_1:def 3
.= Seg (width (0. (R,K))) by MATRIX_0:def 7
.= Seg K by MATRIX_0:24 ;
for k9 being Nat st k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) holds
(Line ((canMat (i,k,I,K,R)),i2)) . k9 = (Line ((0. (R,K)),k)) . k9

proof

let k9 be Nat; :: thesis: ( k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) implies (Line ((canMat (i,k,I,K,R)),i2)) . k9 = (Line ((0. (R,K)),k)) . k9 )
assume A19: k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) ; :: thesis: (Line ((canMat (i,k,I,K,R)),i2)) . k9 = (Line ((0. (R,K)),k)) . k9
then A20: k9 in Seg (width (0. (R,K))) by A6, MATRIX_0:24;
[i2,k] in [:(dom (canMat (i,k,I,K,R))),(Seg (width (canMat (i,k,I,K,R)))):] by A1, MATRIX_0:def 4;
then k in Seg (width (canMat (i,k,I,K,R))) by ZFMISC_1:87;
then k in Seg K by A5, Th43;
then k in Seg (len (0. (R,K))) by MATRIX_0:24;
then k in dom (0. (R,K)) by FINSEQ_1:def 3;
then [k,k9] in [:(dom (0. (R,K))),(Seg (width (0. (R,K)))):] by A20, ZFMISC_1:87;
then A21: [k,k9] in Indices (0. (R,K)) by MATRIX_0:def 4;
A22: k9 in Seg (width (canMat (i,k,I,K,R))) by A5, A6, A19, Th43;
A23: [i2,k9] in Indices (canMat (i,k,I,K,R)) by A4, A19;
thus (Line ((canMat (i,k,I,K,R)),i2)) . k9 = (canMat (i,k,I,K,R)) * (i2,k9) by A22, MATRIX_0:def 7
.= 0. R by A17, A23, Th40
.= (0. (R,K)) * (k,k9) by A21, MATRIX_1:1
.= (Line ((0. (R,K)),k)) . k9 by A20, MATRIX_0:def 7 ; :: thesis: verum

end;

hence Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k) by A6, A18, FINSEQ_1:13; :: thesis: verum

end;

suppose I = 0 ; :: thesis: ( ( i2 = i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((1. (R,K)),k) ) & ( i2 <> i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k) ) )

hence ( ( i2 = i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((1. (R,K)),k) ) & ( i2 <> i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k) ) ) by A1, MATRIX_0:22; :: thesis: verum

end;

suppose A24: ( I <> 0 & not i in dom (canMat (i,k,I,K,R)) ) ; :: thesis: ( ( i2 = i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((1. (R,K)),k) ) & ( i2 <> i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k) ) )

hence ( i2 = i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((1. (R,K)),k) ) by A2; :: thesis: ( i2 <> i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k) )
thus ( i2 <> i implies Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k) ) :: thesis: verum

proof

assume A25: i2 <> i ; :: thesis: Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k)
A26: dom (Line ((canMat (i,k,I,K,R)),i2)) = Seg K by A3, A24, Th43;
set q = Line ((0. (R,K)),k);
A27: dom (Line ((0. (R,K)),k)) = Seg (len (Line ((0. (R,K)),k))) by FINSEQ_1:def 3
.= Seg (width (0. (R,K))) by MATRIX_0:def 7
.= Seg K by MATRIX_0:24 ;
for k9 being Nat st k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) holds
(Line ((canMat (i,k,I,K,R)),i2)) . k9 = (Line ((0. (R,K)),k)) . k9

proof

let k9 be Nat; :: thesis: ( k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) implies (Line ((canMat (i,k,I,K,R)),i2)) . k9 = (Line ((0. (R,K)),k)) . k9 )
assume A28: k9 in dom (Line ((canMat (i,k,I,K,R)),i2)) ; :: thesis: (Line ((canMat (i,k,I,K,R)),i2)) . k9 = (Line ((0. (R,K)),k)) . k9
then A29: k9 in Seg (width (0. (R,K))) by A26, MATRIX_0:24;
[i2,k] in [:(dom (canMat (i,k,I,K,R))),(Seg (width (canMat (i,k,I,K,R)))):] by A1, MATRIX_0:def 4;
then k in Seg (width (canMat (i,k,I,K,R))) by ZFMISC_1:87;
then k in Seg K by A24, Th43;
then k in Seg (len (0. (R,K))) by MATRIX_0:24;
then k in dom (0. (R,K)) by FINSEQ_1:def 3;
then [k,k9] in [:(dom (0. (R,K))),(Seg (width (0. (R,K)))):] by A29, ZFMISC_1:87;
then A30: [k,k9] in Indices (0. (R,K)) by MATRIX_0:def 4;
A31: k9 in Seg (width (canMat (i,k,I,K,R))) by A24, A26, A28, Th43;
A32: [i2,k9] in Indices (canMat (i,k,I,K,R)) by A4, A28;
thus (Line ((canMat (i,k,I,K,R)),i2)) . k9 = (canMat (i,k,I,K,R)) * (i2,k9) by A31, MATRIX_0:def 7
.= 0. R by A25, A32, Th40
.= (0. (R,K)) * (k,k9) by A30, MATRIX_1:1
.= (Line ((0. (R,K)),k)) . k9 by A29, MATRIX_0:def 7 ; :: thesis: verum

end;

hence Line ((canMat (i,k,I,K,R)),i2) = Line ((0. (R,K)),k) by A26, A27, FINSEQ_1:13; :: thesis: verum

end;

end;

end;