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
A27: for m being Nat st 1 <= m & m <= (len f1) - 1 holds
f1 . m = D \ (A . ((len A) - m)) and
A28: for m being Nat st 1 <= m & m <= (len f2) - 1 holds
f2 . m = D \ (A . ((len A) - m)) ; :: thesis: f1 = f2
A29: len f2 = card D by Th1;
A30: len A = card D by Th1;
A31: len f1 = card D by Th1;
then A32: dom f1 = Seg (len A) by A30, FINSEQ_1:def 3;
now :: thesis: for m being Nat st m in dom f1 holds
f1 . m = f2 . m
let m be Nat; :: thesis: ( m in dom f1 implies f1 . b1 = f2 . b1 )
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
assume A33: m in dom f1 ; :: thesis: f1 . b1 = f2 . b1
then A34: 1 <= m by A32, FINSEQ_1:1;
A35: m <= len A by A32, A33, FINSEQ_1:1;
per cases ( m = len A or m <> len A ) ;
suppose A36: m = len A ; :: thesis: f1 . b1 = f2 . b1
then f1 . m = D by A31, A30, Th3;
hence f1 . m = f2 . m by A29, A30, A36, Th3; :: thesis: verum
end;
suppose m <> len A ; :: thesis: f1 . b1 = f2 . b1
then m < len A by A35, XXREAL_0:1;
then m + 1 <= len A by NAT_1:13;
then A37: m <= (len A) - 1 by XREAL_1:19;
then f1 . m1 = D \ (A . ((len A) - m1)) by A27, A31, A30, A34;
hence f1 . m = f2 . m by A28, A29, A30, A34, A37; :: thesis: verum
end;
end;
end;
hence f1 = f2 by A31, A29, FINSEQ_2:9; :: thesis: verum