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:29;

A3: width (GoB (v1,v2)) = len v2 by Def1;

hence GoB (v1,v2) is V3() by A1, MATRIX_0:def 10; :: 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_0:def 4;

thus GoB (v1,v2) is X_equal-in-line :: thesis: GoB (v1,v2) is Y_equal-in-column

A1: len (GoB (v1,v2)) = len v1 by Def1;

then A2: dom (GoB (v1,v2)) = dom v1 by FINSEQ_3:29;

A3: width (GoB (v1,v2)) = len v2 by Def1;

hence GoB (v1,v2) is V3() by A1, MATRIX_0:def 10; :: 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_0:def 4;

thus GoB (v1,v2) is X_equal-in-line :: thesis: GoB (v1,v2) is Y_equal-in-column

proof

thus
GoB (v1,v2) is Y_equal-in-column
:: thesis: verum
let n be Nat; :: according to GOBOARD1:def 4 :: 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_0:def 7;

A7: len (X_axis l) = len l by GOBOARD1:def 1;

then A8: dom (X_axis l) = dom l by FINSEQ_3:29;

end;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_0:def 7;

A7: len (X_axis l) = len l by GOBOARD1:def 1;

then A8: dom (X_axis l) = dom l by FINSEQ_3:29;

now :: thesis: for i, j being Nat st i in dom (X_axis l) & j in dom (X_axis l) holds

(X_axis l) . i = (X_axis l) . j

hence
X_axis (Line ((GoB (v1,v2)),n)) is constant
by SEQM_3:def 10; :: thesis: verum(X_axis l) . i = (X_axis l) . j

let i, j be 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:87;

then (GoB (v1,v2)) * (n,i) = |[r,s1]| by Def1;

then A11: ((GoB (v1,v2)) * (n,i)) `1 = r by EUCLID:52;

l /. i = l . i by A8, A9, PARTFUN1:def 6;

then l /. i = (GoB (v1,v2)) * (n,i) by A7, A6, A9, MATRIX_0:def 7;

then A12: (X_axis l) . i = r by A9, A11, GOBOARD1:def 1;

[n,j] in Indices (GoB (v1,v2)) by A3, A2, A4, A5, A7, A6, A10, ZFMISC_1:87;

then (GoB (v1,v2)) * (n,j) = |[r,s2]| by Def1;

then A13: ((GoB (v1,v2)) * (n,j)) `1 = r by EUCLID:52;

l /. j = l . j by A8, A10, PARTFUN1:def 6;

then l /. j = (GoB (v1,v2)) * (n,j) by A7, A6, A10, MATRIX_0:def 7;

hence (X_axis l) . i = (X_axis l) . j by A10, A13, A12, GOBOARD1:def 1; :: thesis: verum

end;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:87;

then (GoB (v1,v2)) * (n,i) = |[r,s1]| by Def1;

then A11: ((GoB (v1,v2)) * (n,i)) `1 = r by EUCLID:52;

l /. i = l . i by A8, A9, PARTFUN1:def 6;

then l /. i = (GoB (v1,v2)) * (n,i) by A7, A6, A9, MATRIX_0:def 7;

then A12: (X_axis l) . i = r by A9, A11, GOBOARD1:def 1;

[n,j] in Indices (GoB (v1,v2)) by A3, A2, A4, A5, A7, A6, A10, ZFMISC_1:87;

then (GoB (v1,v2)) * (n,j) = |[r,s2]| by Def1;

then A13: ((GoB (v1,v2)) * (n,j)) `1 = r by EUCLID:52;

l /. j = l . j by A8, A10, PARTFUN1:def 6;

then l /. j = (GoB (v1,v2)) * (n,j) by A7, A6, A10, MATRIX_0:def 7;

hence (X_axis l) . i = (X_axis l) . j by A10, A13, A12, GOBOARD1:def 1; :: thesis: verum

proof

let n be Nat; :: according to GOBOARD1:def 5 :: 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 2;

then A14: dom (Y_axis c) = dom c by FINSEQ_3:29;

len c = len (GoB (v1,v2)) by MATRIX_0:def 8;

then A15: dom c = dom (GoB (v1,v2)) by FINSEQ_3:29;

assume A16: n in Seg (width (GoB (v1,v2))) ; :: thesis: Y_axis (Col ((GoB (v1,v2)),n)) is constant

end;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 2;

then A14: dom (Y_axis c) = dom c by FINSEQ_3:29;

len c = len (GoB (v1,v2)) by MATRIX_0:def 8;

then A15: dom c = dom (GoB (v1,v2)) by FINSEQ_3:29;

assume A16: n in Seg (width (GoB (v1,v2))) ; :: thesis: Y_axis (Col ((GoB (v1,v2)),n)) is constant

now :: thesis: for i, j being Nat st i in dom (Y_axis c) & j in dom (Y_axis c) holds

(Y_axis c) . i = (Y_axis c) . j

hence
Y_axis (Col ((GoB (v1,v2)),n)) is constant
by SEQM_3:def 10; :: thesis: verum(Y_axis c) . i = (Y_axis c) . j

let i, j be 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:87;

then (GoB (v1,v2)) * (i,n) = |[s1,r]| by Def1;

then A19: ((GoB (v1,v2)) * (i,n)) `2 = r by EUCLID:52;

c /. i = c . i by A14, A17, PARTFUN1:def 6;

then c /. i = (GoB (v1,v2)) * (i,n) by A14, A15, A17, MATRIX_0:def 8;

then A20: (Y_axis c) . i = r by A17, A19, GOBOARD1:def 2;

[j,n] in Indices (GoB (v1,v2)) by A3, A2, A4, A16, A14, A15, A18, ZFMISC_1:87;

then (GoB (v1,v2)) * (j,n) = |[s2,r]| by Def1;

then A21: ((GoB (v1,v2)) * (j,n)) `2 = r by EUCLID:52;

c /. j = c . j by A14, A18, PARTFUN1:def 6;

then c /. j = (GoB (v1,v2)) * (j,n) by A14, A15, A18, MATRIX_0:def 8;

hence (Y_axis c) . i = (Y_axis c) . j by A18, A21, A20, GOBOARD1:def 2; :: thesis: verum

end;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:87;

then (GoB (v1,v2)) * (i,n) = |[s1,r]| by Def1;

then A19: ((GoB (v1,v2)) * (i,n)) `2 = r by EUCLID:52;

c /. i = c . i by A14, A17, PARTFUN1:def 6;

then c /. i = (GoB (v1,v2)) * (i,n) by A14, A15, A17, MATRIX_0:def 8;

then A20: (Y_axis c) . i = r by A17, A19, GOBOARD1:def 2;

[j,n] in Indices (GoB (v1,v2)) by A3, A2, A4, A16, A14, A15, A18, ZFMISC_1:87;

then (GoB (v1,v2)) * (j,n) = |[s2,r]| by Def1;

then A21: ((GoB (v1,v2)) * (j,n)) `2 = r by EUCLID:52;

c /. j = c . j by A14, A18, PARTFUN1:def 6;

then c /. j = (GoB (v1,v2)) * (j,n) by A14, A15, A18, MATRIX_0:def 8;

hence (Y_axis c) . i = (Y_axis c) . j by A18, A21, A20, GOBOARD1:def 2; :: thesis: verum