let R be non empty ZeroOneStr ; :: thesis: for I, K being Nat holds
not ( ( I = 0 implies K = 0 ) & ( K = 0 implies I = 0 ) & not for i, k being Nat holds (canMat (i,k,I,K,R)) @ = canMat (k,i,K,I,R) )
let I, K be Nat; :: thesis: not ( ( I = 0 implies K = 0 ) & ( K = 0 implies I = 0 ) & not for i, k being Nat holds (canMat (i,k,I,K,R)) @ = canMat (k,i,K,I,R) )
assume A1: ( I = 0 iff K = 0 ) ; :: thesis: for i, k being Nat holds (canMat (i,k,I,K,R)) @ = canMat (k,i,K,I,R)
let i, k be Nat; :: thesis: (canMat (i,k,I,K,R)) @ = canMat (k,i,K,I,R)
set LHS = (canMat (i,k,I,K,R)) @ ;
set RHS = canMat (k,i,K,I,R);

per cases ( I = 0 or I > 0 ) ;

suppose I = 0 ; :: thesis: (canMat (i,k,I,K,R)) @ = canMat (k,i,K,I,R)

then A2: ( (canMat (i,k,I,K,R)) @ is Matrix of 0 ,R & canMat (k,i,K,I,R) is Matrix of 0 ,R ) by A1;
then for i2, j2 being Nat st [i2,j2] in Indices ((canMat (i,k,I,K,R)) @) holds
((canMat (i,k,I,K,R)) @) * (i2,j2) = (canMat (k,i,K,I,R)) * (i2,j2) by MATRIX_0:22;
hence (canMat (i,k,I,K,R)) @ = canMat (k,i,K,I,R) by A2, MATRIX_0:27; :: thesis: verum

end;

suppose A3: I > 0 ; :: thesis: (canMat (i,k,I,K,R)) @ = canMat (k,i,K,I,R)

A4: ( len (canMat (i,k,I,K,R)) = I & width (canMat (i,k,I,K,R)) = K & Indices (canMat (i,k,I,K,R)) = [:(Seg I),(Seg K):] ) by A3, MATRIX_0:23;
then A5: ( len ((canMat (i,k,I,K,R)) @) = K & width ((canMat (i,k,I,K,R)) @) = I ) by A1, A3, MATRIX_0:29;
A6: ( len (canMat (k,i,K,I,R)) = K & width (canMat (k,i,K,I,R)) = I & Indices (canMat (k,i,K,I,R)) = [:(Seg K),(Seg I):] ) by A1, A3, MATRIX_0:23;
for i2, j2 being Nat st [i2,j2] in Indices ((canMat (i,k,I,K,R)) @) holds
((canMat (i,k,I,K,R)) @) * (i2,j2) = (canMat (k,i,K,I,R)) * (i2,j2)

proof

let i2, j2 be Nat; :: thesis: ( [i2,j2] in Indices ((canMat (i,k,I,K,R)) @) implies ((canMat (i,k,I,K,R)) @) * (i2,j2) = (canMat (k,i,K,I,R)) * (i2,j2) )
assume A7: [i2,j2] in Indices ((canMat (i,k,I,K,R)) @) ; :: thesis: ((canMat (i,k,I,K,R)) @) * (i2,j2) = (canMat (k,i,K,I,R)) * (i2,j2)
A8: ( [j2,i2] in Indices (canMat (i,k,I,K,R)) & [i2,j2] in Indices (canMat (k,i,K,I,R)) )

proof

thus [j2,i2] in Indices (canMat (i,k,I,K,R)) by A7, MATRIX_0:def 6; :: thesis: [i2,j2] in Indices (canMat (k,i,K,I,R))
hence [i2,j2] in Indices (canMat (k,i,K,I,R)) by A4, A6, ZFMISC_1:88; :: thesis: verum

end;

per cases ( [k,i] = [i2,j2] or [k,i] <> [i2,j2] ) ;

suppose A9: [k,i] = [i2,j2] ; :: thesis: ((canMat (i,k,I,K,R)) @) * (i2,j2) = (canMat (k,i,K,I,R)) * (i2,j2)

then A10: ( i = j2 & k = i2 ) by XTUPLE_0:1;
thus ((canMat (i,k,I,K,R)) @) * (i2,j2) = (canMat (i,k,I,K,R)) * (j2,i2) by A8, MATRIX_0:def 6
.= 1. R by A8, A10, Def1
.= (canMat (k,i,K,I,R)) * (i2,j2) by A8, A9, Def1 ; :: thesis: verum

end;

suppose A11: [k,i] <> [i2,j2] ; :: thesis: ((canMat (i,k,I,K,R)) @) * (i2,j2) = (canMat (k,i,K,I,R)) * (i2,j2)

A12: [i,k] <> [j2,i2]

proof

assume [i,k] = [j2,i2] ; :: thesis: contradiction
then ( i = j2 & k = i2 ) by XTUPLE_0:1;
hence contradiction by A11; :: thesis: verum

end;

thus ((canMat (i,k,I,K,R)) @) * (i2,j2) = (canMat (i,k,I,K,R)) * (j2,i2) by A8, MATRIX_0:def 6
.= 0. R by A8, A12, Def1
.= (canMat (k,i,K,I,R)) * (i2,j2) by A8, A11, Def1 ; :: thesis: verum

end;

end;

end;

hence (canMat (i,k,I,K,R)) @ = canMat (k,i,K,I,R) by A5, A6, MATRIX_0:21; :: thesis: verum

end;

end;