let f be rectangular special_circular_sequence; :: thesis: GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))
set G = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2));
set v1 = Incr (X_axis f);
set v2 = Incr (Y_axis f);
A1: f /. 2 = N-max (L~ f) by SPRECT_1:84;
A2: f /. 1 = N-min (L~ f) by SPRECT_1:83;
then A3: (f /. 1) `1 < (f /. 2) `1 by A1, SPRECT_2:51;
A4: (f /. 2) `2 = (f /. 1) `2 by A2, A1, PSCOMP_1:37;
A5: f /. 4 = S-min (L~ f) by SPRECT_1:86;
A6: f /. 3 = S-max (L~ f) by SPRECT_1:85;
then A7: (f /. 3) `2 = (f /. 4) `2 by A5, PSCOMP_1:53;
A8: len <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> = 3 by FINSEQ_1:45;
A9: len f = 5 by SPRECT_1:82;
then A10: f /. 1 = f /. 5 by FINSEQ_6:def 1;
set g = <*((f /. 1) `1),((f /. 2) `1)*>;
reconsider h = <*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> as FinSequence of REAL by RVSUM_1:145;
A11: f /. 3 = E-min (L~ f) by SPRECT_1:85;
A12: f /. 2 = E-max (L~ f) by SPRECT_1:84;
then A13: (f /. 3) `1 = (f /. 2) `1 by A11, PSCOMP_1:45;
A14: len <*((f /. 1) `1),((f /. 2) `1)*> = 2 by FINSEQ_1:44;
A15: dom <*((f /. 1) `1),((f /. 2) `1)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
A16: <*((f /. 1) `1),((f /. 2) `1)*> is increasing
proof
A17: <*((f /. 1) `1),((f /. 2) `1)*> . 2 = (f /. 2) `1 by FINSEQ_1:44;
A18: <*((f /. 1) `1),((f /. 2) `1)*> . 1 = (f /. 1) `1 by FINSEQ_1:44;
let n be Nat; :: according to SEQM_3:def 1 :: thesis: for b1 being set holds
( not n in K70(<*((f /. 1) `1),((f /. 2) `1)*>) or not b1 in K70(<*((f /. 1) `1),((f /. 2) `1)*>) or b1 <= n or not <*((f /. 1) `1),((f /. 2) `1)*> . b1 <= <*((f /. 1) `1),((f /. 2) `1)*> . n )
let m be Nat; :: thesis: ( not n in K70(<*((f /. 1) `1),((f /. 2) `1)*>) or not m in K70(<*((f /. 1) `1),((f /. 2) `1)*>) or m <= n or not <*((f /. 1) `1),((f /. 2) `1)*> . m <= <*((f /. 1) `1),((f /. 2) `1)*> . n )
assume that
A19: n in dom <*((f /. 1) `1),((f /. 2) `1)*> and
A20: m in dom <*((f /. 1) `1),((f /. 2) `1)*> and
A21: n < m ; :: thesis: not <*((f /. 1) `1),((f /. 2) `1)*> . m <= <*((f /. 1) `1),((f /. 2) `1)*> . n
A22: ( m = 1 or m = 2 ) by A15, A20, TARSKI:def 2;
( n = 1 or n = 2 ) by A15, A19, TARSKI:def 2;
hence <*((f /. 1) `1),((f /. 2) `1)*> . n < <*((f /. 1) `1),((f /. 2) `1)*> . m by A2, A1, A21, A18, A17, A22, SPRECT_2:51; :: thesis: verum
end;
A23: f /. 4 = W-min (L~ f) by SPRECT_1:86;
A24: len h = (len <*((f /. 1) `1),((f /. 2) `1)*>) + (len <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) by FINSEQ_1:22
.= (len <*((f /. 1) `1),((f /. 2) `1)*>) + 3 by FINSEQ_1:45
.= 2 + 3 by FINSEQ_1:44
.= len f by SPRECT_1:82 ;
for n being Nat st n in dom h holds
h . n = (f /. n) `1
proof
let n be Nat; :: thesis: ( n in dom h implies h . n = (f /. n) `1 )
assume A25: n in dom h ; :: thesis: h . n = (f /. n) `1
then A26: 1 <= n by FINSEQ_3:25;
n <= 5 by A9, A24, A25, FINSEQ_3:25;
then not not n = 0 & ... & not n = 5 ;
per cases then ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A26;
suppose A27: n = 1 ; :: thesis: h . n = (f /. n) `1
then n in dom <*((f /. 1) `1),((f /. 2) `1)*> by A14, FINSEQ_3:25;
hence h . n = <*((f /. 1) `1),((f /. 2) `1)*> . 1 by A27, FINSEQ_1:def 7
.= (f /. n) `1 by A27, FINSEQ_1:44 ;
:: thesis: verum
end;
suppose A28: n = 2 ; :: thesis: h . n = (f /. n) `1
then n in dom <*((f /. 1) `1),((f /. 2) `1)*> by A14, FINSEQ_3:25;
hence h . n = <*((f /. 1) `1),((f /. 2) `1)*> . 2 by A28, FINSEQ_1:def 7
.= (f /. n) `1 by A28, FINSEQ_1:44 ;
:: thesis: verum
end;
suppose A29: n = 3 ; :: thesis: h . n = (f /. n) `1
hence h . n = h . (2 + 1)
.= <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> . 1 by A14, A8, FINSEQ_1:65
.= (f /. n) `1 by A29, FINSEQ_1:45 ;
:: thesis: verum
end;
suppose A30: n = 4 ; :: thesis: h . n = (f /. n) `1
hence h . n = h . (2 + 2)
.= <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> . 2 by A14, A8, FINSEQ_1:65
.= (f /. n) `1 by A30, FINSEQ_1:45 ;
:: thesis: verum
end;
suppose A31: n = 5 ; :: thesis: h . n = (f /. n) `1
hence h . n = h . (2 + 3)
.= <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> . 3 by A14, A8, FINSEQ_1:65
.= (f /. n) `1 by A31, FINSEQ_1:45 ;
:: thesis: verum
end;
end;
end;
then A32: X_axis f = h by A24, GOBOARD1:def 1;
A33: rng <*((f /. 1) `1),((f /. 2) `1)*> = {((f /. 1) `1),((f /. 2) `1)} by FINSEQ_2:127;
A34: f /. 1 = W-max (L~ f) by SPRECT_1:83;
then A35: (f /. 4) `2 < (f /. 5) `2 by A23, A10, SPRECT_2:57;
reconsider vv1 = <*((f /. 1) `1),((f /. 2) `1)*> as FinSequence of REAL by RVSUM_1:145;
{((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)} c= {((f /. 1) `1),((f /. 2) `1)}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)} or x in {((f /. 1) `1),((f /. 2) `1)} )
assume A36: x in {((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)} ; :: thesis: x in {((f /. 1) `1),((f /. 2) `1)}
per cases ( x = (f /. 3) `1 or x = (f /. 4) `1 or x = (f /. 5) `1 ) by A36, ENUMSET1:def 1;
suppose x = (f /. 3) `1 ; :: thesis: x in {((f /. 1) `1),((f /. 2) `1)}
then x = (f /. 2) `1 by A12, A11, PSCOMP_1:45;
hence x in {((f /. 1) `1),((f /. 2) `1)} by TARSKI:def 2; :: thesis: verum
end;
suppose x = (f /. 4) `1 ; :: thesis: x in {((f /. 1) `1),((f /. 2) `1)}
then x = (f /. 1) `1 by A34, A23, PSCOMP_1:29;
hence x in {((f /. 1) `1),((f /. 2) `1)} by TARSKI:def 2; :: thesis: verum
end;
suppose x = (f /. 5) `1 ; :: thesis: x in {((f /. 1) `1),((f /. 2) `1)}
then x = (f /. 1) `1 by A9, FINSEQ_6:def 1;
hence x in {((f /. 1) `1),((f /. 2) `1)} by TARSKI:def 2; :: thesis: verum
end;
end;
end;
then A37: rng <*((f /. 1) `1),((f /. 2) `1)*> = (rng <*((f /. 1) `1),((f /. 2) `1)*>) \/ {((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)} by A33, XBOOLE_1:12
.= (rng <*((f /. 1) `1),((f /. 2) `1)*>) \/ (rng <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>) by FINSEQ_2:128
.= rng (X_axis f) by A32, FINSEQ_1:31 ;
len <*((f /. 1) `1),((f /. 2) `1)*> = 2 by FINSEQ_1:44
.= card (rng (X_axis f)) by A33, A37, A3, CARD_2:57 ;
then A38: Incr (X_axis f) = vv1 by A37, A16, SEQ_4:def 21;
then A39: (Incr (X_axis f)) . 1 = (f /. 1) `1 by FINSEQ_1:44;
set g = <*((f /. 4) `2),((f /. 5) `2)*>;
reconsider h = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*> as FinSequence of REAL by RVSUM_1:145;
A40: len h = (len <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*>) + (len <*((f /. 4) `2),((f /. 5) `2)*>) by FINSEQ_1:22
.= (len <*((f /. 4) `2),((f /. 5) `2)*>) + 3 by FINSEQ_1:45
.= 2 + 3 by FINSEQ_1:44
.= len f by SPRECT_1:82 ;
A41: len <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> = 3 by FINSEQ_1:45;
A42: dom <*((f /. 4) `2),((f /. 5) `2)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
A43: <*((f /. 4) `2),((f /. 5) `2)*> is increasing
proof
A44: <*((f /. 4) `2),((f /. 5) `2)*> . 2 = (f /. 5) `2 by FINSEQ_1:44;
A45: <*((f /. 4) `2),((f /. 5) `2)*> . 1 = (f /. 4) `2 by FINSEQ_1:44;
let n be Nat; :: according to SEQM_3:def 1 :: thesis: for b1 being set holds
( not n in K70(<*((f /. 4) `2),((f /. 5) `2)*>) or not b1 in K70(<*((f /. 4) `2),((f /. 5) `2)*>) or b1 <= n or not <*((f /. 4) `2),((f /. 5) `2)*> . b1 <= <*((f /. 4) `2),((f /. 5) `2)*> . n )
let m be Nat; :: thesis: ( not n in K70(<*((f /. 4) `2),((f /. 5) `2)*>) or not m in K70(<*((f /. 4) `2),((f /. 5) `2)*>) or m <= n or not <*((f /. 4) `2),((f /. 5) `2)*> . m <= <*((f /. 4) `2),((f /. 5) `2)*> . n )
assume that
A46: n in dom <*((f /. 4) `2),((f /. 5) `2)*> and
A47: m in dom <*((f /. 4) `2),((f /. 5) `2)*> and
A48: n < m ; :: thesis: not <*((f /. 4) `2),((f /. 5) `2)*> . m <= <*((f /. 4) `2),((f /. 5) `2)*> . n
A49: ( m = 1 or m = 2 ) by A42, A47, TARSKI:def 2;
( n = 1 or n = 2 ) by A42, A46, TARSKI:def 2;
hence <*((f /. 4) `2),((f /. 5) `2)*> . n < <*((f /. 4) `2),((f /. 5) `2)*> . m by A34, A23, A10, A48, A45, A44, A49, SPRECT_2:57; :: thesis: verum
end;
A50: (Incr (X_axis f)) . 2 = (f /. 2) `1 by A38, FINSEQ_1:44;
A51: len <*((f /. 4) `2),((f /. 5) `2)*> = 2 by FINSEQ_1:44;
for n being Nat st n in dom h holds
h . n = (f /. n) `2
proof
let n be Nat; :: thesis: ( n in dom h implies h . n = (f /. n) `2 )
assume A52: n in dom h ; :: thesis: h . n = (f /. n) `2
then A53: 1 <= n by FINSEQ_3:25;
n <= 5 by A9, A40, A52, FINSEQ_3:25;
then not not n = 0 & ... & not n = 5 ;
per cases then ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A53;
suppose A54: n = 1 ; :: thesis: h . n = (f /. n) `2
then n in dom <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> by A41, FINSEQ_3:25;
hence h . n = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> . 1 by A54, FINSEQ_1:def 7
.= (f /. n) `2 by A54, FINSEQ_1:45 ;
:: thesis: verum
end;
suppose A55: n = 2 ; :: thesis: h . n = (f /. n) `2
then n in dom <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> by A41, FINSEQ_3:25;
hence h . n = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> . 2 by A55, FINSEQ_1:def 7
.= (f /. n) `2 by A55, FINSEQ_1:45 ;
:: thesis: verum
end;
suppose A56: n = 3 ; :: thesis: h . n = (f /. n) `2
then n in dom <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> by A41, FINSEQ_3:25;
hence h . n = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> . 3 by A56, FINSEQ_1:def 7
.= (f /. n) `2 by A56, FINSEQ_1:45 ;
:: thesis: verum
end;
suppose A57: n = 4 ; :: thesis: h . n = (f /. n) `2
hence h . n = h . (3 + 1)
.= <*((f /. 4) `2),((f /. 5) `2)*> . 1 by A51, A41, FINSEQ_1:65
.= (f /. n) `2 by A57, FINSEQ_1:44 ;
:: thesis: verum
end;
suppose A58: n = 5 ; :: thesis: h . n = (f /. n) `2
hence h . n = h . (2 + 3)
.= <*((f /. 4) `2),((f /. 5) `2)*> . 2 by A51, A41, FINSEQ_1:65
.= (f /. n) `2 by A58, FINSEQ_1:44 ;
:: thesis: verum
end;
end;
end;
then A59: Y_axis f = h by A40, GOBOARD1:def 2;
A60: rng <*((f /. 4) `2),((f /. 5) `2)*> = {((f /. 4) `2),((f /. 5) `2)} by FINSEQ_2:127;
{((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)} c= {((f /. 4) `2),((f /. 5) `2)}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)} or x in {((f /. 4) `2),((f /. 5) `2)} )
assume A61: x in {((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)} ; :: thesis: x in {((f /. 4) `2),((f /. 5) `2)}
per cases ( x = (f /. 1) `2 or x = (f /. 2) `2 or x = (f /. 3) `2 ) by A61, ENUMSET1:def 1;
suppose x = (f /. 1) `2 ; :: thesis: x in {((f /. 4) `2),((f /. 5) `2)}
hence x in {((f /. 4) `2),((f /. 5) `2)} by A10, TARSKI:def 2; :: thesis: verum
end;
suppose x = (f /. 2) `2 ; :: thesis: x in {((f /. 4) `2),((f /. 5) `2)}
then x = (f /. 1) `2 by A2, A1, PSCOMP_1:37;
hence x in {((f /. 4) `2),((f /. 5) `2)} by A10, TARSKI:def 2; :: thesis: verum
end;
suppose x = (f /. 3) `2 ; :: thesis: x in {((f /. 4) `2),((f /. 5) `2)}
then x = (f /. 4) `2 by A6, A5, PSCOMP_1:53;
hence x in {((f /. 4) `2),((f /. 5) `2)} by TARSKI:def 2; :: thesis: verum
end;
end;
end;
then A62: rng <*((f /. 4) `2),((f /. 5) `2)*> = {((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)} \/ {((f /. 4) `2),((f /. 5) `2)} by A60, XBOOLE_1:12
.= (rng <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*>) \/ {((f /. 4) `2),((f /. 5) `2)} by FINSEQ_2:128
.= (rng <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*>) \/ (rng <*((f /. 4) `2),((f /. 5) `2)*>) by FINSEQ_2:127
.= rng (Y_axis f) by A59, FINSEQ_1:31 ;
reconsider vv2 = <*((f /. 4) `2),((f /. 1) `2)*> as FinSequence of REAL by RVSUM_1:145;
len <*((f /. 4) `2),((f /. 5) `2)*> = 2 by FINSEQ_1:44
.= card (rng (Y_axis f)) by A60, A62, A35, CARD_2:57 ;
then A63: Incr (Y_axis f) = vv2 by A10, A62, A43, SEQ_4:def 21;
then A64: (Incr (Y_axis f)) . 1 = (f /. 4) `2 by FINSEQ_1:44;
A65: (Incr (Y_axis f)) . 2 = (f /. 1) `2 by A63, FINSEQ_1:44;
A66: (f /. 1) `1 = (f /. 4) `1 by A34, A23, PSCOMP_1:29;
A67: for n, m being Nat st [n,m] in Indices (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) holds
(((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
proof
let n, m be Nat; :: thesis: ( [n,m] in Indices (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) implies (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| )
assume [n,m] in Indices (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) ; :: thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A68: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by Th2;
per cases ( [n,m] = [1,1] or [n,m] = [1,2] or [n,m] = [2,1] or [n,m] = [2,2] ) by A68, ENUMSET1:def 2;
suppose A69: [n,m] = [1,1] ; :: thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A70: m = 1 by XTUPLE_0:1;
A71: n = 1 by A69, XTUPLE_0:1;
hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 4 by A70, MATRIX_0:50
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A39, A64, A66, A71, A70, EUCLID:53 ;
:: thesis: verum
end;
suppose A72: [n,m] = [1,2] ; :: thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A73: m = 2 by XTUPLE_0:1;
A74: n = 1 by A72, XTUPLE_0:1;
hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 1 by A73, MATRIX_0:50
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A39, A65, A74, A73, EUCLID:53 ;
:: thesis: verum
end;
suppose A75: [n,m] = [2,1] ; :: thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A76: m = 1 by XTUPLE_0:1;
A77: n = 2 by A75, XTUPLE_0:1;
hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 3 by A76, MATRIX_0:50
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A50, A64, A13, A7, A77, A76, EUCLID:53 ;
:: thesis: verum
end;
suppose A78: [n,m] = [2,2] ; :: thesis: (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]|
then A79: m = 2 by XTUPLE_0:1;
A80: n = 2 by A78, XTUPLE_0:1;
hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 2 by A79, MATRIX_0:50
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A50, A65, A4, A80, A79, EUCLID:53 ;
:: thesis: verum
end;
end;
end;
A81: width (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) = 2 by MATRIX_0:47
.= len (Incr (Y_axis f)) by A63, FINSEQ_1:44 ;
len (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) = 2 by MATRIX_0:47
.= len (Incr (X_axis f)) by A38, FINSEQ_1:44 ;
then GoB ((Incr (X_axis f)),(Incr (Y_axis f))) = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) by A81, A67, GOBOARD2:def 1;
hence GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) by GOBOARD2:def 2; :: thesis: verum