let f1, f2 be RearrangmentGen of D; :: thesis: ( ( for m being Nat st 1 <= m & m <= (len f1) - 1 holds
f1 . m = D \ (A . ((len A) - m)) ) & ( for m being Nat st 1 <= m & m <= (len f2) - 1 holds
f2 . m = D \ (A . ((len A) - m)) ) implies f1 = f2 )
assume that
A29: for m being Nat st 1 <= m & m <= (len f1) - 1 holds
f1 . m = D \ (A . ((len A) - m)) and
A30: for m being Nat st 1 <= m & m <= (len f2) - 1 holds
f2 . m = D \ (A . ((len A) - m)) ; :: thesis: f1 = f2
A31: ( len f1 = card D & len f2 = card D & len A = card D ) by Th1;
then X: dom f1 = Seg (len A) by FINSEQ_1:def 3;

now

let m be Nat; :: thesis: ( m in dom f1 implies f1 . m = f2 . m )
assume m in dom f1 ; :: thesis: f1 . m = f2 . m
then A32: ( 1 <= m & m <= len A ) by X, FINSEQ_1:3;
reconsider m1 = m as Element of NAT by ORDINAL1:def 13;

now

per cases ( m = len A or m <> len A ) ;

case m = len A ; :: thesis: f1 . m = f2 . m

then ( f1 . m = D & f2 . m = D ) by A31, Th3;
hence f1 . m = f2 . m ; :: thesis: verum

end;

case m <> len A ; :: thesis: f1 . m = f2 . m

then m < len A by A32, XXREAL_0:1;
then m + 1 <= len A by NAT_1:13;
then m <= (len A) - 1 by XREAL_1:21;
then ( f1 . m1 = D \ (A . ((len A) - m1)) & f2 . m1 = D \ (A . ((len A) - m1)) ) by A29, A30, A31, A32;
hence f1 . m = f2 . m ; :: thesis: verum

end;

end;

end;

hence f1 . m = f2 . m ; :: thesis: verum

end;

hence f1 = f2 by A31, FINSEQ_2:10; :: thesis: verum