let B, A be RearrangmentGen of D; :: thesis: ( ( for m being Nat st 1 <= m & m <= (len B) - 1 holds
B . m = D \ (A . ((len A) - m)) ) implies for m being Nat st 1 <= m & m <= (len A) - 1 holds
A . m = D \ (B . ((len B) - m)) )
assume A38: for m being Nat st 1 <= m & m <= (len B) - 1 holds
B . m = D \ (A . ((len A) - m)) ; :: thesis: for m being Nat st 1 <= m & m <= (len A) - 1 holds
A . m = D \ (B . ((len B) - m))
let m be Nat; :: thesis: ( 1 <= m & m <= (len A) - 1 implies A . m = D \ (B . ((len B) - m)) )
assume A39: ( 1 <= m & m <= (len A) - 1 ) ; :: thesis: A . m = D \ (B . ((len B) - m))
A40: len A = card D by Th1;
A41: len B = card D by Th1;
(len A) - 1 < len A by XREAL_1:44;
then A42: m < len A by A39, XXREAL_0:2;
then (len A) - m in NAT by INT_1:5;
then reconsider n = (len B) - m as Nat by A40, A41;
A43: (len A) - n = m by A40, A41;
m + 1 <= len A by A39, XREAL_1:19;
then A44: 1 <= n by A40, A41, XREAL_1:19;
A45: n <= (len B) - 1 by A39, XREAL_1:10;
(len A) - n in dom A by A43, A39, A42, FINSEQ_3:25;
then A46: A . ((len A) - n) c= D by Lm5;
thus A . m = A . ((len A) - n) by A40, A41
.= D /\ (A . ((len A) - n)) by A46, XBOOLE_1:28
.= D \ (D \ (A . ((len A) - n))) by XBOOLE_1:48
.= D \ (B . ((len B) - m)) by A44, A45, A38 ; :: thesis: verum