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 /. 1 = N-min (L~ f) & f /. 1 = W-max (L~ f) ) by SPRECT_1:91;
A2: ( f /. 2 = N-max (L~ f) & f /. 2 = E-max (L~ f) ) by SPRECT_1:92;
A3: ( f /. 3 = S-max (L~ f) & f /. 3 = E-min (L~ f) ) by SPRECT_1:93;
A4: ( f /. 4 = S-min (L~ f) & f /. 4 = W-min (L~ f) ) by SPRECT_1:94;
A5: len f = 5 by SPRECT_1:90;
set g = <*((f /. 1) `1 ),((f /. 2) `1 )*>;
set h = <*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>;
A6: len <*((f /. 1) `1 ),((f /. 2) `1 )*> = 2 by FINSEQ_1:61;
A7: len <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*> = 3 by FINSEQ_1:62;
A8: len (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) = (len <*((f /. 1) `1 ),((f /. 2) `1 )*>) + (len <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) by FINSEQ_1:35
.= (len <*((f /. 1) `1 ),((f /. 2) `1 )*>) + 3 by FINSEQ_1:62
.= 2 + 3 by FINSEQ_1:61
.= len f by SPRECT_1:90 ;
for n being Element of NAT st n in dom (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) holds
(<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . n = (f /. n) `1
proof
let n be Element of NAT ; :: thesis: ( n in dom (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) implies (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . n = (f /. n) `1 )
assume n in dom (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) ; :: thesis: (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . n = (f /. n) `1
then A9: ( 1 <= n & n <= 5 ) by A5, A8, FINSEQ_3:27;
per cases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A9, NAT_1:30;
suppose A10: n = 1 ; :: thesis: (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . n = (f /. n) `1
then n in dom <*((f /. 1) `1 ),((f /. 2) `1 )*> by A6, FINSEQ_3:27;
hence (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . n = <*((f /. 1) `1 ),((f /. 2) `1 )*> . 1 by A10, FINSEQ_1:def 7
.= (f /. n) `1 by A10, FINSEQ_1:61 ;
:: thesis: verum
end;
suppose A11: n = 2 ; :: thesis: (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . n = (f /. n) `1
then n in dom <*((f /. 1) `1 ),((f /. 2) `1 )*> by A6, FINSEQ_3:27;
hence (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . n = <*((f /. 1) `1 ),((f /. 2) `1 )*> . 2 by A11, FINSEQ_1:def 7
.= (f /. n) `1 by A11, FINSEQ_1:61 ;
:: thesis: verum
end;
suppose A12: n = 3 ; :: thesis: (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . n = (f /. n) `1
hence (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . n = (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . (2 + 1)
.= <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*> . 1 by A6, A7, FINSEQ_1:86
.= (f /. n) `1 by A12, FINSEQ_1:62 ;
:: thesis: verum
end;
suppose A13: n = 4 ; :: thesis: (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . n = (f /. n) `1
hence (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . n = (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . (2 + 2)
.= <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*> . 2 by A6, A7, FINSEQ_1:86
.= (f /. n) `1 by A13, FINSEQ_1:62 ;
:: thesis: verum
end;
suppose A14: n = 5 ; :: thesis: (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . n = (f /. n) `1
hence (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . n = (<*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) . (2 + 3)
.= <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*> . 3 by A6, A7, FINSEQ_1:86
.= (f /. n) `1 by A14, FINSEQ_1:62 ;
:: thesis: verum
end;
end;
end;
then A15: X_axis f = <*((f /. 1) `1 ),((f /. 2) `1 )*> ^ <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*> by A8, GOBOARD1:def 3;
A16: dom <*((f /. 1) `1 ),((f /. 2) `1 )*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
A17: {((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )} c= {((f /. 1) `1 ),((f /. 2) `1 )}
proof
let x be set ; :: 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 A18: 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 A18, ENUMSET1:def 1;
suppose x = (f /. 3) `1 ; :: thesis: x in {((f /. 1) `1 ),((f /. 2) `1 )}
then x = (f /. 2) `1 by A2, A3, PSCOMP_1:105;
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 A1, A4, PSCOMP_1:85;
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 A5, FINSEQ_6:def 1;
hence x in {((f /. 1) `1 ),((f /. 2) `1 )} by TARSKI:def 2; :: thesis: verum
end;
end;
end;
A19: rng <*((f /. 1) `1 ),((f /. 2) `1 )*> = {((f /. 1) `1 ),((f /. 2) `1 )} by FINSEQ_2:147;
then A20: rng <*((f /. 1) `1 ),((f /. 2) `1 )*> = (rng <*((f /. 1) `1 ),((f /. 2) `1 )*>) \/ {((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )} by A17, XBOOLE_1:12
.= (rng <*((f /. 1) `1 ),((f /. 2) `1 )*>) \/ (rng <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*>) by FINSEQ_2:148
.= rng (X_axis f) by A15, FINSEQ_1:44 ;
A21: (f /. 1) `1 < (f /. 2) `1 by A1, A2, SPRECT_2:55;
A22: len <*((f /. 1) `1 ),((f /. 2) `1 )*> = 2 by FINSEQ_1:61
.= card (rng (X_axis f)) by A19, A20, A21, CARD_2:76 ;
<*((f /. 1) `1 ),((f /. 2) `1 )*> is increasing
proof
let n be Element of NAT ; :: according to SEQM_3:def 1 :: thesis: for b1 being Element of NAT holds
( not n in K6(<*((f /. 1) `1 ),((f /. 2) `1 )*>) or not b1 in K6(<*((f /. 1) `1 ),((f /. 2) `1 )*>) or b1 <= n or not K550(<*((f /. 1) `1 ),((f /. 2) `1 )*>,b1) <= K550(<*((f /. 1) `1 ),((f /. 2) `1 )*>,n) )
let m be Element of NAT ; :: thesis: ( not n in K6(<*((f /. 1) `1 ),((f /. 2) `1 )*>) or not m in K6(<*((f /. 1) `1 ),((f /. 2) `1 )*>) or m <= n or not K550(<*((f /. 1) `1 ),((f /. 2) `1 )*>,m) <= K550(<*((f /. 1) `1 ),((f /. 2) `1 )*>,n) )
assume that
A23: n in dom <*((f /. 1) `1 ),((f /. 2) `1 )*> and
A24: m in dom <*((f /. 1) `1 ),((f /. 2) `1 )*> and
A25: n < m ; :: thesis: not K550(<*((f /. 1) `1 ),((f /. 2) `1 )*>,m) <= K550(<*((f /. 1) `1 ),((f /. 2) `1 )*>,n)
A26: ( <*((f /. 1) `1 ),((f /. 2) `1 )*> . 1 = (f /. 1) `1 & <*((f /. 1) `1 ),((f /. 2) `1 )*> . 2 = (f /. 2) `1 ) by FINSEQ_1:61;
( ( n = 1 or n = 2 ) & ( m = 1 or m = 2 ) ) by A16, A23, A24, TARSKI:def 2;
hence <*((f /. 1) `1 ),((f /. 2) `1 )*> . n < <*((f /. 1) `1 ),((f /. 2) `1 )*> . m by A1, A2, A25, A26, SPRECT_2:55; :: thesis: verum
end;
then A27: Incr (X_axis f) = <*((f /. 1) `1 ),((f /. 2) `1 )*> by A20, A22, GOBOARD2:def 2;
set g = <*((f /. 4) `2 ),((f /. 5) `2 )*>;
set h = <*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>;
A28: len <*((f /. 4) `2 ),((f /. 5) `2 )*> = 2 by FINSEQ_1:61;
A29: len <*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> = 3 by FINSEQ_1:62;
A30: len (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) = (len <*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*>) + (len <*((f /. 4) `2 ),((f /. 5) `2 )*>) by FINSEQ_1:35
.= (len <*((f /. 4) `2 ),((f /. 5) `2 )*>) + 3 by FINSEQ_1:62
.= 2 + 3 by FINSEQ_1:61
.= len f by SPRECT_1:90 ;
for n being Element of NAT st n in dom (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) holds
(<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . n = (f /. n) `2
proof
let n be Element of NAT ; :: thesis: ( n in dom (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) implies (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . n = (f /. n) `2 )
assume n in dom (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) ; :: thesis: (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . n = (f /. n) `2
then A31: ( 1 <= n & n <= 5 ) by A5, A30, FINSEQ_3:27;
per cases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A31, NAT_1:30;
suppose A32: n = 1 ; :: thesis: (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . n = (f /. n) `2
then n in dom <*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> by A29, FINSEQ_3:27;
hence (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . n = <*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> . 1 by A32, FINSEQ_1:def 7
.= (f /. n) `2 by A32, FINSEQ_1:62 ;
:: thesis: verum
end;
suppose A33: n = 2 ; :: thesis: (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . n = (f /. n) `2
then n in dom <*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> by A29, FINSEQ_3:27;
hence (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . n = <*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> . 2 by A33, FINSEQ_1:def 7
.= (f /. n) `2 by A33, FINSEQ_1:62 ;
:: thesis: verum
end;
suppose A34: n = 3 ; :: thesis: (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . n = (f /. n) `2
then n in dom <*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> by A29, FINSEQ_3:27;
hence (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . n = <*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> . 3 by A34, FINSEQ_1:def 7
.= (f /. n) `2 by A34, FINSEQ_1:62 ;
:: thesis: verum
end;
suppose A35: n = 4 ; :: thesis: (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . n = (f /. n) `2
hence (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . n = (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . (3 + 1)
.= <*((f /. 4) `2 ),((f /. 5) `2 )*> . 1 by A28, A29, FINSEQ_1:86
.= (f /. n) `2 by A35, FINSEQ_1:61 ;
:: thesis: verum
end;
suppose A36: n = 5 ; :: thesis: (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . n = (f /. n) `2
hence (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . n = (<*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*>) . (2 + 3)
.= <*((f /. 4) `2 ),((f /. 5) `2 )*> . 2 by A28, A29, FINSEQ_1:86
.= (f /. n) `2 by A36, FINSEQ_1:61 ;
:: thesis: verum
end;
end;
end;
then A37: Y_axis f = <*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> ^ <*((f /. 4) `2 ),((f /. 5) `2 )*> by A30, GOBOARD1:def 4;
A38: dom <*((f /. 4) `2 ),((f /. 5) `2 )*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
A39: f /. 1 = f /. 5 by A5, FINSEQ_6:def 1;
A40: {((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )} c= {((f /. 4) `2 ),((f /. 5) `2 )}
proof
let x be set ; :: 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 A41: 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 A41, 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 A39, 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 A1, A2, PSCOMP_1:95;
hence x in {((f /. 4) `2 ),((f /. 5) `2 )} by A39, 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 A3, A4, PSCOMP_1:115;
hence x in {((f /. 4) `2 ),((f /. 5) `2 )} by TARSKI:def 2; :: thesis: verum
end;
end;
end;
A42: rng <*((f /. 4) `2 ),((f /. 5) `2 )*> = {((f /. 4) `2 ),((f /. 5) `2 )} by FINSEQ_2:147;
then A43: rng <*((f /. 4) `2 ),((f /. 5) `2 )*> = {((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )} \/ {((f /. 4) `2 ),((f /. 5) `2 )} by A40, XBOOLE_1:12
.= (rng <*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*>) \/ {((f /. 4) `2 ),((f /. 5) `2 )} by FINSEQ_2:148
.= (rng <*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*>) \/ (rng <*((f /. 4) `2 ),((f /. 5) `2 )*>) by FINSEQ_2:147
.= rng (Y_axis f) by A37, FINSEQ_1:44 ;
A44: (f /. 4) `2 < (f /. 5) `2 by A1, A4, A39, SPRECT_2:61;
A45: len <*((f /. 4) `2 ),((f /. 5) `2 )*> = 2 by FINSEQ_1:61
.= card (rng (Y_axis f)) by A42, A43, A44, CARD_2:76 ;
<*((f /. 4) `2 ),((f /. 5) `2 )*> is increasing
proof
let n be Element of NAT ; :: according to SEQM_3:def 1 :: thesis: for b1 being Element of NAT holds
( not n in K6(<*((f /. 4) `2 ),((f /. 5) `2 )*>) or not b1 in K6(<*((f /. 4) `2 ),((f /. 5) `2 )*>) or b1 <= n or not K550(<*((f /. 4) `2 ),((f /. 5) `2 )*>,b1) <= K550(<*((f /. 4) `2 ),((f /. 5) `2 )*>,n) )
let m be Element of NAT ; :: thesis: ( not n in K6(<*((f /. 4) `2 ),((f /. 5) `2 )*>) or not m in K6(<*((f /. 4) `2 ),((f /. 5) `2 )*>) or m <= n or not K550(<*((f /. 4) `2 ),((f /. 5) `2 )*>,m) <= K550(<*((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 K550(<*((f /. 4) `2 ),((f /. 5) `2 )*>,m) <= K550(<*((f /. 4) `2 ),((f /. 5) `2 )*>,n)
A49: ( <*((f /. 4) `2 ),((f /. 5) `2 )*> . 1 = (f /. 4) `2 & <*((f /. 4) `2 ),((f /. 5) `2 )*> . 2 = (f /. 5) `2 ) by FINSEQ_1:61;
( ( n = 1 or n = 2 ) & ( m = 1 or m = 2 ) ) by A38, A46, A47, TARSKI:def 2;
hence <*((f /. 4) `2 ),((f /. 5) `2 )*> . n < <*((f /. 4) `2 ),((f /. 5) `2 )*> . m by A1, A4, A39, A48, A49, SPRECT_2:61; :: thesis: verum
end;
then A50: Incr (Y_axis f) = <*((f /. 4) `2 ),((f /. 1) `2 )*> by A39, A43, A45, GOBOARD2:def 2;
A51: len ((f /. 4),(f /. 1) ][ (f /. 3),(f /. 2)) = 2 by MATRIX_2:3
.= len (Incr (X_axis f)) by A27, FINSEQ_1:61 ;
A52: width ((f /. 4),(f /. 1) ][ (f /. 3),(f /. 2)) = 2 by MATRIX_2:3
.= len (Incr (Y_axis f)) by A50, FINSEQ_1:61 ;
A53: (Incr (X_axis f)) . 1 = (f /. 1) `1 by A27, FINSEQ_1:61;
A54: (Incr (X_axis f)) . 2 = (f /. 2) `1 by A27, FINSEQ_1:61;
A55: (Incr (Y_axis f)) . 1 = (f /. 4) `2 by A50, FINSEQ_1:61;
A56: (Incr (Y_axis f)) . 2 = (f /. 1) `2 by A50, FINSEQ_1:61;
A57: (f /. 1) `1 = (f /. 4) `1 by A1, A4, PSCOMP_1:85;
A58: (f /. 3) `1 = (f /. 2) `1 by A2, A3, PSCOMP_1:105;
A59: (f /. 3) `2 = (f /. 4) `2 by A3, A4, PSCOMP_1:115;
A60: (f /. 2) `2 = (f /. 1) `2 by A1, A2, PSCOMP_1:95;
for n, m being Element of 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 Element of 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 A61: [n,m] in {[1,1],[1,2],[2,1],[2,2]} by Th12;
per cases ( [n,m] = [1,1] or [n,m] = [1,2] or [n,m] = [2,1] or [n,m] = [2,2] ) by A61, ENUMSET1:def 2;
suppose [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 A62: ( n = 1 & m = 1 ) by ZFMISC_1:33;
hence ((f /. 4),(f /. 1) ][ (f /. 3),(f /. 2)) * n,m = f /. 4 by MATRIX_2:6
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A53, A55, A57, A62, EUCLID:57 ;
:: thesis: verum
end;
suppose [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 A63: ( n = 1 & m = 2 ) by ZFMISC_1:33;
hence ((f /. 4),(f /. 1) ][ (f /. 3),(f /. 2)) * n,m = f /. 1 by MATRIX_2:6
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A53, A56, A63, EUCLID:57 ;
:: thesis: verum
end;
suppose [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 A64: ( n = 2 & m = 1 ) by ZFMISC_1:33;
hence ((f /. 4),(f /. 1) ][ (f /. 3),(f /. 2)) * n,m = f /. 3 by MATRIX_2:6
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A54, A55, A58, A59, A64, EUCLID:57 ;
:: thesis: verum
end;
suppose [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 A65: ( n = 2 & m = 2 ) by ZFMISC_1:33;
hence ((f /. 4),(f /. 1) ][ (f /. 3),(f /. 2)) * n,m = f /. 2 by MATRIX_2:6
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A54, A56, A60, A65, EUCLID:57 ;
:: thesis: verum
end;
end;
end;
then GoB (Incr (X_axis f)),(Incr (Y_axis f)) = (f /. 4),(f /. 1) ][ (f /. 3),(f /. 2) by A51, A52, GOBOARD2:def 1;
hence GoB f = (f /. 4),(f /. 1) ][ (f /. 3),(f /. 2) by GOBOARD2:def 3; :: thesis: verum