let i, j be 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:1;
then A6: Y_axis (Col (G,j)) is constant by A1;
reconsider c = Col (G,j) as FinSequence of (TOP-REAL 2) ;
A7: i in dom G by A4, A5, FINSEQ_3:25;
A8: 1 <= len G by A4, A5, XXREAL_0:2;
then A9: 1 in dom G by FINSEQ_3:25;
A10: len c = len G by MATRIX_0:def 8;
then 1 in dom c by A8, FINSEQ_3:25;
then A11: c /. 1 = c . 1 by PARTFUN1:def 6;
i in dom c by A4, A5, A10, FINSEQ_3:25;
then A12: c /. i = c . i by PARTFUN1:def 6;
A13: len (Y_axis (Col (G,j))) = len c by GOBOARD1:def 2;
then A14: 1 in dom (Y_axis (Col (G,j))) by A8, A10, FINSEQ_3:25;
A15: i in dom (Y_axis (Col (G,j))) by A4, A5, A10, A13, FINSEQ_3:25;
thus (G * (i,j)) `2 = (c /. i) `2 by A7, A12, MATRIX_0:def 8
.= (Y_axis (Col (G,j))) . i by A15, GOBOARD1:def 2
.= (Y_axis (Col (G,j))) . 1 by A6, A14, A15
.= (c /. 1) `2 by A14, GOBOARD1:def 2
.= (G * (1,j)) `2 by A9, A11, MATRIX_0:def 8 ; :: thesis: verum