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:92;
A2: f /. 1 = N-min (L~ f) by SPRECT_1:91;
then A3: (f /. 1) `1 < (f /. 2) `1 by A1, SPRECT_2:55;
A4: (f /. 2) `2 = (f /. 1) `2 by A2, A1, PSCOMP_1:95;
A5: f /. 4 = S-min (L~ f) by SPRECT_1:94;
A6: f /. 3 = S-max (L~ f) by SPRECT_1:93;
then A7: (f /. 3) `2 = (f /. 4) `2 by A5, PSCOMP_1:115;
A8: len <*((f /. 3) `1 ),((f /. 4) `1 ),((f /. 5) `1 )*> = 3 by FINSEQ_1:62;
A9: len f = 5 by SPRECT_1:90;
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:93;
A12: f /. 2 = E-max (L~ f) by SPRECT_1:92;
then A13: (f /. 3) `1 = (f /. 2) `1 by A11, PSCOMP_1:105;
A14: len <*((f /. 1) `1 ),((f /. 2) `1 )*> = 2 by FINSEQ_1:61;
A15: dom <*((f /. 1) `1 ),((f /. 2) `1 )*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
A16: <*((f /. 1) `1 ),((f /. 2) `1 )*> is increasing
proof
A17: <*((f /. 1) `1 ),((f /. 2) `1 )*> . 2 = (f /. 2) `1 by FINSEQ_1:61;
A18: <*((f /. 1) `1 ),((f /. 2) `1 )*> . 1 = (f /. 1) `1 by FINSEQ_1:61;
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 K555(<*((f /. 1) `1 ),((f /. 2) `1 )*>,b1) <= K555(<*((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 K555(<*((f /. 1) `1 ),((f /. 2) `1 )*>,m) <= K555(<*((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 K555(<*((f /. 1) `1 ),((f /. 2) `1 )*>,m) <= K555(<*((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:55; :: thesis: verum
end;
A23: f /. 4 = W-min (L~ f) by SPRECT_1:94;
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: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 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:27;
A27: n <= 5 by A9, A24, A25, FINSEQ_3:27;
per cases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A26, A27, NAT_1:30;
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: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 A28, FINSEQ_1:def 7
.= (f /. n) `1 by A28, FINSEQ_1:61 ;
:: 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: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 A29, FINSEQ_1:def 7
.= (f /. n) `1 by A29, FINSEQ_1:61 ;
:: 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:86
.= (f /. n) `1 by A30, FINSEQ_1:62 ;
:: 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:86
.= (f /. n) `1 by A31, FINSEQ_1:62 ;
:: 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:86
.= (f /. n) `1 by A32, FINSEQ_1:62 ;
:: 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 3;
A34: rng <*((f /. 1) `1 ),((f /. 2) `1 )*> = {((f /. 1) `1 ),((f /. 2) `1 )} by FINSEQ_2:147;
A35: f /. 1 = W-max (L~ f) by SPRECT_1:91;
then A36: (f /. 4) `2 < (f /. 5) `2 by A23, A10, SPRECT_2:61;
{((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: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 A35, A23, 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 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:148
.= rng (X_axis f) by A33, FINSEQ_1:44 ;
len <*((f /. 1) `1 ),((f /. 2) `1 )*> = 2 by FINSEQ_1:61
.= card (rng (X_axis f)) by A34, A38, A3, CARD_2:76 ;
then A39: Incr (X_axis f) = <*((f /. 1) `1 ),((f /. 2) `1 )*> by A38, A16, SEQ_4:def 25;
then A40: (Incr (X_axis f)) . 1 = (f /. 1) `1 by FINSEQ_1:61;
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: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 ;
A42: len <*((f /. 1) `2 ),((f /. 2) `2 ),((f /. 3) `2 )*> = 3 by FINSEQ_1:62;
A43: dom <*((f /. 4) `2 ),((f /. 5) `2 )*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
A44: <*((f /. 4) `2 ),((f /. 5) `2 )*> is increasing
proof
A45: <*((f /. 4) `2 ),((f /. 5) `2 )*> . 2 = (f /. 5) `2 by FINSEQ_1:61;
A46: <*((f /. 4) `2 ),((f /. 5) `2 )*> . 1 = (f /. 4) `2 by FINSEQ_1:61;
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 K555(<*((f /. 4) `2 ),((f /. 5) `2 )*>,b1) <= K555(<*((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 K555(<*((f /. 4) `2 ),((f /. 5) `2 )*>,m) <= K555(<*((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 K555(<*((f /. 4) `2 ),((f /. 5) `2 )*>,m) <= K555(<*((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:61; :: thesis: verum
end;
A51: (Incr (X_axis f)) . 2 = (f /. 2) `1 by A39, FINSEQ_1:61;
A52: len <*((f /. 4) `2 ),((f /. 5) `2 )*> = 2 by FINSEQ_1:61;
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:27;
A55: n <= 5 by A9, A41, A53, FINSEQ_3:27;
per cases ( n = 1 or n = 2 or n = 3 or n = 4 or n = 5 ) by A54, A55, NAT_1:30;
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: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 A56, FINSEQ_1:def 7
.= (f /. n) `2 by A56, FINSEQ_1:62 ;
:: 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: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 A57, FINSEQ_1:def 7
.= (f /. n) `2 by A57, FINSEQ_1:62 ;
:: 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: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 A58, FINSEQ_1:def 7
.= (f /. n) `2 by A58, FINSEQ_1:62 ;
:: 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:86
.= (f /. n) `2 by A59, FINSEQ_1:61 ;
:: 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:86
.= (f /. n) `2 by A60, FINSEQ_1:61 ;
:: 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 4;
A62: rng <*((f /. 4) `2 ),((f /. 5) `2 )*> = {((f /. 4) `2 ),((f /. 5) `2 )} by FINSEQ_2:147;
{((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:95;
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:115;
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: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 A61, FINSEQ_1:44 ;
len <*((f /. 4) `2 ),((f /. 5) `2 )*> = 2 by FINSEQ_1:61
.= card (rng (Y_axis f)) by A62, A64, A36, CARD_2:76 ;
then A65: Incr (Y_axis f) = <*((f /. 4) `2 ),((f /. 1) `2 )*> by A10, A64, A44, SEQ_4:def 25;
then A66: (Incr (Y_axis f)) . 1 = (f /. 4) `2 by FINSEQ_1:61;
A67: (Incr (Y_axis f)) . 2 = (f /. 1) `2 by A65, FINSEQ_1:61;
A68: (f /. 1) `1 = (f /. 4) `1 by A35, A23, PSCOMP_1:85;
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:33;
A73: n = 1 by A71, ZFMISC_1:33;
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:57 ;
:: 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:33;
A76: n = 1 by A74, ZFMISC_1:33;
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:57 ;
:: 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:33;
A79: n = 2 by A77, ZFMISC_1:33;
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:57 ;
:: 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:33;
A82: n = 2 by A80, ZFMISC_1:33;
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:57 ;
:: 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:61 ;
len ((f /. 4),(f /. 1) ][ (f /. 3),(f /. 2)) = 2 by MATRIX_2:3
.= len (Incr (X_axis f)) by A39, FINSEQ_1:61 ;
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 3; :: thesis: verum