let s, s1 be State of SCMPDS; :: thesis: for n0, n1, n2, n being Nat
for f, f1 being FinSequence of INT st f is_FinSequence_on s,n0 & f1 is_FinSequence_on s1,n0 & len f = n & len f1 = n & ( for i being Nat st i >= n0 + 1 & i <> n1 & i <> n2 holds
s1 . (intpos i) = s . (intpos i) ) & ( ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) or ( n1 >= n0 + 1 & n2 >= n0 + 1 & n1 <= n0 + n & n2 <= n0 + n & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ) holds
f,f1 are_fiberwise_equipotent
let n0, n1, n2, n be Nat; :: thesis: for f, f1 being FinSequence of INT st f is_FinSequence_on s,n0 & f1 is_FinSequence_on s1,n0 & len f = n & len f1 = n & ( for i being Nat st i >= n0 + 1 & i <> n1 & i <> n2 holds
s1 . (intpos i) = s . (intpos i) ) & ( ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) or ( n1 >= n0 + 1 & n2 >= n0 + 1 & n1 <= n0 + n & n2 <= n0 + n & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ) holds
f,f1 are_fiberwise_equipotent
let f, f1 be FinSequence of INT ; :: thesis: ( f is_FinSequence_on s,n0 & f1 is_FinSequence_on s1,n0 & len f = n & len f1 = n & ( for i being Nat st i >= n0 + 1 & i <> n1 & i <> n2 holds
s1 . (intpos i) = s . (intpos i) ) & ( ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) or ( n1 >= n0 + 1 & n2 >= n0 + 1 & n1 <= n0 + n & n2 <= n0 + n & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ) implies f,f1 are_fiberwise_equipotent )
assume that
A1: f is_FinSequence_on s,n0 and
A2: f1 is_FinSequence_on s1,n0 ; :: thesis: ( not len f = n or not len f1 = n or ex i being Nat st
( i >= n0 + 1 & i <> n1 & i <> n2 & not s1 . (intpos i) = s . (intpos i) ) or ( not ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) & not ( n1 >= n0 + 1 & n2 >= n0 + 1 & n1 <= n0 + n & n2 <= n0 + n & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ) or f,f1 are_fiberwise_equipotent )
assume that
A3: len f = n and
A4: len f1 = n ; :: thesis: ( ex i being Nat st
( i >= n0 + 1 & i <> n1 & i <> n2 & not s1 . (intpos i) = s . (intpos i) ) or ( not ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) & not ( n1 >= n0 + 1 & n2 >= n0 + 1 & n1 <= n0 + n & n2 <= n0 + n & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ) or f,f1 are_fiberwise_equipotent )
assume A5: for i being Nat st i >= n0 + 1 & i <> n1 & i <> n2 holds
s1 . (intpos i) = s . (intpos i) ; :: thesis: ( ( not ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) & not ( n1 >= n0 + 1 & n2 >= n0 + 1 & n1 <= n0 + n & n2 <= n0 + n & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ) or f,f1 are_fiberwise_equipotent )
assume A6: ( ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) or ( n1 >= n0 + 1 & n2 >= n0 + 1 & n1 <= n0 + n & n2 <= n0 + n & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ) ; :: thesis: f,f1 are_fiberwise_equipotent
per cases ( ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) or ( n1 >= n0 + 1 & n2 >= n0 + 1 & n1 <= n0 + n & n2 <= n0 + n & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ) by A6;
suppose A7: ( s1 . (intpos n1) = s . (intpos n1) & s1 . (intpos n2) = s . (intpos n2) ) ; :: thesis: f,f1 are_fiberwise_equipotent
A8: dom f1 = Seg n by A4, FINSEQ_1:def 3;
now :: thesis: for i being Nat st i in dom f1 holds
f1 . i = f . i
let i be Nat; :: thesis: ( i in dom f1 implies f1 . b1 = f . b1 )
reconsider a = i as Nat ;
assume A9: i in dom f1 ; :: thesis: f1 . b1 = f . b1
then A10: 1 <= i by A8, FINSEQ_1:1;
then A11: n0 + 1 <= n0 + i by XREAL_1:6;
A12: i <= n by A8, A9, FINSEQ_1:1;
per cases ( ( n0 + i <> n1 & n0 + i <> n2 ) or not n0 + i <> n1 or not n0 + i <> n2 ) ;
suppose A13: ( n0 + i <> n1 & n0 + i <> n2 ) ; :: thesis: f1 . b1 = f . b1
thus f1 . i = s1 . (intpos (n0 + a)) by A2, A4, A10, A12
.= s . (intpos (n0 + a)) by A5, A11, A13
.= f . i by A1, A3, A10, A12 ; :: thesis: verum
end;
suppose A14: ( not n0 + i <> n1 or not n0 + i <> n2 ) ; :: thesis: f1 . b1 = f . b1
hereby :: thesis: verum
per cases ( n0 + i = n1 or n0 + i = n2 ) by A14;
suppose n0 + i = n1 ; :: thesis: f1 . i = f . i
hence f1 . i = s . (intpos (n0 + a)) by A2, A4, A7, A10, A12
.= f . i by A1, A3, A10, A12 ;
:: thesis: verum
end;
suppose n0 + i = n2 ; :: thesis: f1 . i = f . i
hence f1 . i = s . (intpos (n0 + a)) by A2, A4, A7, A10, A12
.= f . i by A1, A3, A10, A12 ;
:: thesis: verum
end;
end;
end;
end;
end;
end;
hence f,f1 are_fiberwise_equipotent by A3, A4, FINSEQ_2:9; :: thesis: verum
end;
suppose A15: ( n1 >= n0 + 1 & n2 >= n0 + 1 & n1 <= n0 + n & n2 <= n0 + n & s1 . (intpos n1) = s . (intpos n2) & s1 . (intpos n2) = s . (intpos n1) ) ; :: thesis: f,f1 are_fiberwise_equipotent
then A16: n1 - n0 >= 1 by XREAL_1:19;
then reconsider m1 = n1 - n0 as Element of NAT by INT_1:3;
A17: m1 <= len f by A3, A15, XREAL_1:20;
A18: n2 - n0 >= 1 by A15, XREAL_1:19;
then reconsider m2 = n2 - n0 as Element of NAT by INT_1:3;
A19: m2 <= len f1 by A4, A15, XREAL_1:20;
A20: n2 = m2 + n0 ;
A21: n1 = m1 + n0 ;
then A22: f . m1 = s1 . (intpos n2) by A1, A15, A16, A17
.= f1 . m2 by A2, A18, A19, A20 ;
A23: now :: thesis: for k being Nat st k <> m1 & k <> m2 & 1 <= k & k <= len f holds
f . k = f1 . k
let k be Nat; :: thesis: ( k <> m1 & k <> m2 & 1 <= k & k <= len f implies f . k = f1 . k )
assume that
A24: k <> m1 and
A25: k <> m2 and
A26: 1 <= k and
A27: k <= len f ; :: thesis: f . k = f1 . k
A28: k + n0 <> m1 + n0 by A24;
A29: n0 + 1 <= n0 + k by A26, XREAL_1:6;
A30: k + n0 <> m2 + n0 by A25;
thus f . k = s . (intpos (k + n0)) by A1, A26, A27
.= s1 . (intpos (k + n0)) by A5, A28, A30, A29
.= f1 . k by A2, A3, A4, A26, A27 ; :: thesis: verum
end;
A31: m2 <= len f by A3, A15, XREAL_1:20;
then f . m2 = s1 . (intpos n1) by A1, A15, A18, A20
.= f1 . m1 by A2, A3, A4, A16, A17, A21 ;
hence f,f1 are_fiberwise_equipotent by A3, A4, A16, A18, A17, A31, A22, A23, SCPISORT:3; :: thesis: verum
end;
end;