let j, i be Element of NAT ; :: thesis: for G being Matrix of (TOP-REAL 2) st G is Y_equal-in-column & 1 <= j & j <= width G & 1 <= i & i <= len G holds
(G * i,j) `2 = (G * 1,j) `2
let G be Matrix of (TOP-REAL 2); :: thesis: ( G is Y_equal-in-column & 1 <= j & j <= width G & 1 <= i & i <= len G implies (G * i,j) `2 = (G * 1,j) `2 )
assume that
A1: G is Y_equal-in-column and
A2: 1 <= j and
A3: j <= width G and
A4: 1 <= i and
A5: i <= len G ; :: thesis: (G * i,j) `2 = (G * 1,j) `2
j in Seg (width G) by A2, A3, FINSEQ_1:3;
then A6: Y_axis (Col G,j) is constant by A1, GOBOARD1:def 7;
reconsider c = Col G,j as FinSequence of (TOP-REAL 2) ;
A7: i in dom G by A4, A5, FINSEQ_3:27;
A8: 1 <= len G by A4, A5, XXREAL_0:2;
then A9: 1 in dom G by FINSEQ_3:27;
A10: len c = len G by MATRIX_1:def 9;
then 1 in dom c by A8, FINSEQ_3:27;
then A11: c /. 1 = c . 1 by PARTFUN1:def 8;
i in dom c by A4, A5, A10, FINSEQ_3:27;
then A12: c /. i = c . i by PARTFUN1:def 8;
A13: len (Y_axis (Col G,j)) = len c by GOBOARD1:def 4;
then A14: 1 in dom (Y_axis (Col G,j)) by A8, A10, FINSEQ_3:27;
A15: i in dom (Y_axis (Col G,j)) by A4, A5, A10, A13, FINSEQ_3:27;
thus (G * i,j) `2 = (c /. i) `2 by A7, A12, MATRIX_1:def 9
.= (Y_axis (Col G,j)) . i by A15, GOBOARD1:def 4
.= (Y_axis (Col G,j)) . 1 by A6, A14, A15, SEQM_3:def 15
.= (c /. 1) `2 by A14, GOBOARD1:def 4
.= (G * 1,j) `2 by A9, A11, MATRIX_1:def 9 ; :: thesis: verum