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)*>;
set h = <*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*>;
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 Element of NAT ; :: according to SEQM_3:def 1 :: thesis: for b1 being Element of NAT holds
( not n in K58(<*((f /. 1) `1),((f /. 2) `1)*>) or not b1 in K58(<*((f /. 1) `1),((f /. 2) `1)*>) or b1 <= n or not K556(<*((f /. 1) `1),((f /. 2) `1)*>,b1) <= K556(<*((f /. 1) `1),((f /. 2) `1)*>,n) )
let m be Element of NAT ; :: thesis: ( not n in K58(<*((f /. 1) `1),((f /. 2) `1)*>) or not m in K58(<*((f /. 1) `1),((f /. 2) `1)*>) or m <= n or not K556(<*((f /. 1) `1),((f /. 2) `1)*>,m) <= K556(<*((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 K556(<*((f /. 1) `1),((f /. 2) `1)*>,m) <= K556(<*((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 (<*((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: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 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 A25: 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 A26: 1 <= n by FINSEQ_3:25;
A27: n <= 5 by A9, A24, A25, FINSEQ_3:25;
per cases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A26, A27, NAT_1:29;
suppose A28: 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 A14, FINSEQ_3:25;
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 A28, FINSEQ_1:def 7
.= (f /. n) `1 by A28, FINSEQ_1:44 ;
:: thesis: verum
end;
suppose A29: 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 A14, FINSEQ_3:25;
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 A29, FINSEQ_1:def 7
.= (f /. n) `1 by A29, FINSEQ_1:44 ;
:: thesis: verum
end;
suppose A30: 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 A14, A8, FINSEQ_1:65
.= (f /. n) `1 by A30, FINSEQ_1:45 ;
:: thesis: verum
end;
suppose A31: 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 A14, A8, FINSEQ_1:65
.= (f /. n) `1 by A31, FINSEQ_1:45 ;
:: thesis: verum
end;
suppose A32: 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 A14, A8, FINSEQ_1:65
.= (f /. n) `1 by A32, FINSEQ_1:45 ;
:: thesis: verum
end;
end;
end;
then A33: X_axis f = <*((f /. 1) `1),((f /. 2) `1)*> ^ <*((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)*> by A24, GOBOARD1:def 1;
A34: rng <*((f /. 1) `1),((f /. 2) `1)*> = {((f /. 1) `1),((f /. 2) `1)} by FINSEQ_2:127;
A35: f /. 1 = W-max (L~ f) by SPRECT_1:83;
then A36: (f /. 4) `2 < (f /. 5) `2 by A23, A10, SPRECT_2:57;
{((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 A37: 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 A37, 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 A35, 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 A38: rng <*((f /. 1) `1),((f /. 2) `1)*> = (rng <*((f /. 1) `1),((f /. 2) `1)*>) \/ {((f /. 3) `1),((f /. 4) `1),((f /. 5) `1)} by A34, 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 A33, FINSEQ_1:31 ;
len <*((f /. 1) `1),((f /. 2) `1)*> = 2 by FINSEQ_1:44
.= card (rng (X_axis f)) by A34, A38, A3, CARD_2:57 ;
then A39: Incr (X_axis f) = <*((f /. 1) `1),((f /. 2) `1)*> by A38, A16, SEQ_4:def 21;
then A40: (Incr (X_axis f)) . 1 = (f /. 1) `1 by FINSEQ_1:44;
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)*>;
A41: 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: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 ;
A42: len <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> = 3 by FINSEQ_1:45;
A43: dom <*((f /. 4) `2),((f /. 5) `2)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
A44: <*((f /. 4) `2),((f /. 5) `2)*> is increasing
proof
A45: <*((f /. 4) `2),((f /. 5) `2)*> . 2 = (f /. 5) `2 by FINSEQ_1:44;
A46: <*((f /. 4) `2),((f /. 5) `2)*> . 1 = (f /. 4) `2 by FINSEQ_1:44;
let n be Element of NAT ; :: according to SEQM_3:def 1 :: thesis: for b1 being Element of NAT holds
( not n in K58(<*((f /. 4) `2),((f /. 5) `2)*>) or not b1 in K58(<*((f /. 4) `2),((f /. 5) `2)*>) or b1 <= n or not K556(<*((f /. 4) `2),((f /. 5) `2)*>,b1) <= K556(<*((f /. 4) `2),((f /. 5) `2)*>,n) )
let m be Element of NAT ; :: thesis: ( not n in K58(<*((f /. 4) `2),((f /. 5) `2)*>) or not m in K58(<*((f /. 4) `2),((f /. 5) `2)*>) or m <= n or not K556(<*((f /. 4) `2),((f /. 5) `2)*>,m) <= K556(<*((f /. 4) `2),((f /. 5) `2)*>,n) )
assume that
A47: n in dom <*((f /. 4) `2),((f /. 5) `2)*> and
A48: m in dom <*((f /. 4) `2),((f /. 5) `2)*> and
A49: n < m ; :: thesis: not K556(<*((f /. 4) `2),((f /. 5) `2)*>,m) <= K556(<*((f /. 4) `2),((f /. 5) `2)*>,n)
A50: ( m = 1 or m = 2 ) by A43, A48, TARSKI:def 2;
( n = 1 or n = 2 ) by A43, A47, TARSKI:def 2;
hence <*((f /. 4) `2),((f /. 5) `2)*> . n < <*((f /. 4) `2),((f /. 5) `2)*> . m by A35, A23, A10, A49, A46, A45, A50, SPRECT_2:57; :: thesis: verum
end;
A51: (Incr (X_axis f)) . 2 = (f /. 2) `1 by A39, FINSEQ_1:44;
A52: len <*((f /. 4) `2),((f /. 5) `2)*> = 2 by FINSEQ_1:44;
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 A53: 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 A54: 1 <= n by FINSEQ_3:25;
A55: n <= 5 by A9, A41, A53, FINSEQ_3:25;
per cases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A54, A55, NAT_1:29;
suppose A56: 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 A42, FINSEQ_3:25;
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 A56, FINSEQ_1:def 7
.= (f /. n) `2 by A56, FINSEQ_1:45 ;
:: thesis: verum
end;
suppose A57: 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 A42, FINSEQ_3:25;
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 A57, FINSEQ_1:def 7
.= (f /. n) `2 by A57, FINSEQ_1:45 ;
:: thesis: verum
end;
suppose A58: 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 A42, FINSEQ_3:25;
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 A58, FINSEQ_1:def 7
.= (f /. n) `2 by A58, FINSEQ_1:45 ;
:: thesis: verum
end;
suppose A59: 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 A52, A42, FINSEQ_1:65
.= (f /. n) `2 by A59, FINSEQ_1:44 ;
:: thesis: verum
end;
suppose A60: 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 A52, A42, FINSEQ_1:65
.= (f /. n) `2 by A60, FINSEQ_1:44 ;
:: thesis: verum
end;
end;
end;
then A61: Y_axis f = <*((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)*> ^ <*((f /. 4) `2),((f /. 5) `2)*> by A41, GOBOARD1:def 2;
A62: 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 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 A63: 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 A63, 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 A64: rng <*((f /. 4) `2),((f /. 5) `2)*> = {((f /. 1) `2),((f /. 2) `2),((f /. 3) `2)} \/ {((f /. 4) `2),((f /. 5) `2)} by A62, 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 A61, FINSEQ_1:31 ;
len <*((f /. 4) `2),((f /. 5) `2)*> = 2 by FINSEQ_1:44
.= card (rng (Y_axis f)) by A62, A64, A36, CARD_2:57 ;
then A65: Incr (Y_axis f) = <*((f /. 4) `2),((f /. 1) `2)*> by A10, A64, A44, SEQ_4:def 21;
then A66: (Incr (Y_axis f)) . 1 = (f /. 4) `2 by FINSEQ_1:44;
A67: (Incr (Y_axis f)) . 2 = (f /. 1) `2 by A65, FINSEQ_1:44;
A68: (f /. 1) `1 = (f /. 4) `1 by A35, A23, PSCOMP_1:29;
A69: 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 A70: [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 A70, ENUMSET1:def 2;
suppose A71: [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 A72: m = 1 by ZFMISC_1:27;
A73: n = 1 by A71, ZFMISC_1:27;
hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 4 by A72, MATRIX_2:6
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A40, A66, A68, A73, A72, EUCLID:53 ;
:: thesis: verum
end;
suppose A74: [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 A75: m = 2 by ZFMISC_1:27;
A76: n = 1 by A74, ZFMISC_1:27;
hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 1 by A75, MATRIX_2:6
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A40, A67, A76, A75, EUCLID:53 ;
:: thesis: verum
end;
suppose A77: [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 A78: m = 1 by ZFMISC_1:27;
A79: n = 2 by A77, ZFMISC_1:27;
hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 3 by A78, MATRIX_2:6
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A51, A66, A13, A7, A79, A78, EUCLID:53 ;
:: thesis: verum
end;
suppose A80: [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 A81: m = 2 by ZFMISC_1:27;
A82: n = 2 by A80, ZFMISC_1:27;
hence (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) * (n,m) = f /. 2 by A81, MATRIX_2:6
.= |[((Incr (X_axis f)) . n),((Incr (Y_axis f)) . m)]| by A51, A67, A4, A82, A81, EUCLID:53 ;
:: thesis: verum
end;
end;
end;
A83: width (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) = 2 by MATRIX_2:3
.= len (Incr (Y_axis f)) by A65, FINSEQ_1:44 ;
len (((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2))) = 2 by MATRIX_2:3
.= len (Incr (X_axis f)) by A39, FINSEQ_1:44 ;
then GoB ((Incr (X_axis f)),(Incr (Y_axis f))) = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) by A83, A69, GOBOARD2:def 1;
hence GoB f = ((f /. 4),(f /. 1)) ][ ((f /. 3),(f /. 2)) by GOBOARD2:def 2; :: thesis: verum