set M = GoB v1,v2;
A1: len (GoB v1,v2) = len v1 by Def1;
then A2: dom (GoB v1,v2) = dom v1 by FINSEQ_3:31;
A3: width (GoB v1,v2) = len v2 by Def1;
hence not GoB v1,v2 is empty-yielding by A1, GOBOARD1:def 5; :: thesis: ( GoB v1,v2 is X_equal-in-line & GoB v1,v2 is Y_equal-in-column )
A4: Indices (GoB v1,v2) = [:(dom v1),(Seg (len v2)):] by A3, A2, MATRIX_1:def 5;
thus GoB v1,v2 is X_equal-in-line :: thesis: GoB v1,v2 is Y_equal-in-column

proof

let n be Element of NAT ; :: according to GOBOARD1:def 6 :: thesis: ( not n in dom (GoB v1,v2) or X_axis (Line (GoB v1,v2),n) is constant )
reconsider l = Line (GoB v1,v2),n as FinSequence of (TOP-REAL 2) ;
set x = X_axis l;
assume A5: n in dom (GoB v1,v2) ; :: thesis: X_axis (Line (GoB v1,v2),n) is constant
A6: ( len l = width (GoB v1,v2) & dom (X_axis l) = Seg (len (X_axis l)) ) by FINSEQ_1:def 3, MATRIX_1:def 8;
A7: len (X_axis l) = len l by GOBOARD1:def 3;
then A8: dom (X_axis l) = dom l by FINSEQ_3:31;

now

let i, j be Element of NAT ; :: thesis: ( i in dom (X_axis l) & j in dom (X_axis l) implies (X_axis l) . i = (X_axis l) . j )
assume that
A9: i in dom (X_axis l) and
A10: j in dom (X_axis l) ; :: thesis: (X_axis l) . i = (X_axis l) . j
reconsider r = v1 . n, s1 = v2 . i, s2 = v2 . j as Real ;
[n,i] in Indices (GoB v1,v2) by A3, A2, A4, A5, A7, A6, A9, ZFMISC_1:106;
then (GoB v1,v2) * n,i = |[r,s1]| by Def1;
then A11: ((GoB v1,v2) * n,i) `1 = r by EUCLID:56;
l /. i = l . i by A8, A9, PARTFUN1:def 8;
then l /. i = (GoB v1,v2) * n,i by A7, A6, A9, MATRIX_1:def 8;
then A12: (X_axis l) . i = r by A9, A11, GOBOARD1:def 3;
[n,j] in Indices (GoB v1,v2) by A3, A2, A4, A5, A7, A6, A10, ZFMISC_1:106;
then (GoB v1,v2) * n,j = |[r,s2]| by Def1;
then A13: ((GoB v1,v2) * n,j) `1 = r by EUCLID:56;
l /. j = l . j by A8, A10, PARTFUN1:def 8;
then l /. j = (GoB v1,v2) * n,j by A7, A6, A10, MATRIX_1:def 8;
hence (X_axis l) . i = (X_axis l) . j by A10, A13, A12, GOBOARD1:def 3; :: thesis: verum

end;

hence X_axis (Line (GoB v1,v2),n) is constant by GOBOARD1:def 2; :: thesis: verum

end;

thus GoB v1,v2 is Y_equal-in-column :: thesis: verum

proof

let n be Element of NAT ; :: according to GOBOARD1:def 7 :: thesis: ( not n in Seg (width (GoB v1,v2)) or Y_axis (Col (GoB v1,v2),n) is constant )
reconsider c = Col (GoB v1,v2),n as FinSequence of (TOP-REAL 2) ;
set y = Y_axis c;
len (Y_axis c) = len c by GOBOARD1:def 4;
then A14: dom (Y_axis c) = dom c by FINSEQ_3:31;
len c = len (GoB v1,v2) by MATRIX_1:def 9;
then A15: dom c = dom (GoB v1,v2) by FINSEQ_3:31;
assume A16: n in Seg (width (GoB v1,v2)) ; :: thesis: Y_axis (Col (GoB v1,v2),n) is constant

now

let i, j be Element of NAT ; :: thesis: ( i in dom (Y_axis c) & j in dom (Y_axis c) implies (Y_axis c) . i = (Y_axis c) . j )
assume that
A17: i in dom (Y_axis c) and
A18: j in dom (Y_axis c) ; :: thesis: (Y_axis c) . i = (Y_axis c) . j
reconsider r = v2 . n, s1 = v1 . i, s2 = v1 . j as Real ;
[i,n] in Indices (GoB v1,v2) by A3, A2, A4, A16, A14, A15, A17, ZFMISC_1:106;
then (GoB v1,v2) * i,n = |[s1,r]| by Def1;
then A19: ((GoB v1,v2) * i,n) `2 = r by EUCLID:56;
c /. i = c . i by A14, A17, PARTFUN1:def 8;
then c /. i = (GoB v1,v2) * i,n by A14, A15, A17, MATRIX_1:def 9;
then A20: (Y_axis c) . i = r by A17, A19, GOBOARD1:def 4;
[j,n] in Indices (GoB v1,v2) by A3, A2, A4, A16, A14, A15, A18, ZFMISC_1:106;
then (GoB v1,v2) * j,n = |[s2,r]| by Def1;
then A21: ((GoB v1,v2) * j,n) `2 = r by EUCLID:56;
c /. j = c . j by A14, A18, PARTFUN1:def 8;
then c /. j = (GoB v1,v2) * j,n by A14, A15, A18, MATRIX_1:def 9;
hence (Y_axis c) . i = (Y_axis c) . j by A18, A21, A20, GOBOARD1:def 4; :: thesis: verum

end;

hence Y_axis (Col (GoB v1,v2),n) is constant by GOBOARD1:def 2; :: thesis: verum

end;