take o = the DoubleReorganization of dom f; :: thesis:
thus for n being Nat ex x being object st x = f . (o _ (n,1)) & ... & x = f . (o _ (n,(len (o . n)))) :: thesis:

let n be Nat; :: thesis:
take x = {} ; :: thesis:
thus x = f . (o _ (n,1)) & ... & x = f . (o _ (n,(len (o . n)))) by A1; :: thesis:

end;

let n1, n2, i1, i2 be Nat; :: thesis:
thus ( i1 in dom (o . n1) & i2 in dom (o . n2) & f . (o _ (n1,i1)) = f . (o _ (n2,i2)) implies n1 = n2 ) by A1; :: thesis:

end;

then reconsider F = rng f as non empty finite set ;
set c = the one-to-one onto FinSequence of F;
A2: rng the one-to-one onto FinSequence of F = F by FUNCT_2:def 3;
then reconsider C = the one-to-one onto FinSequence of F as non empty FinSequence ;
consider o being len C -element DoubleReorganization of dom f such that
A3: for n being Nat holds the one-to-one onto FinSequence of F . n = f . (o _ (n,1)) & ... & the one-to-one onto FinSequence of F . n = f . (o _ (n,(len (o . n)))) by Th38, A2;
take o ; :: thesis:
thus for n being Nat ex x being object st x = f . (o _ (n,1)) & ... & x = f . (o _ (n,(len (o . n)))) :: thesis:

let n be Nat; :: thesis:
take x = the one-to-one onto FinSequence of F . n; :: thesis:
let i be Nat; :: thesis:
assume A4: ( 1 <= i & i <= len (o . n) ) ; :: thesis:
the one-to-one onto FinSequence of F . n = f . (o _ (n,1)) & ... & the one-to-one onto FinSequence of F . n = f . (o _ (n,(len (o . n)))) by A3;
hence x = f . (o _ (n,i)) by A4; :: thesis:

end;

let n1, n2, i1, i2 be Nat; :: thesis:
assume A5: ( i1 in dom (o . n1) & i2 in dom (o . n2) & f . (o _ (n1,i1)) = f . (o _ (n2,i2)) ) ; :: thesis:
A6: the one-to-one onto FinSequence of F . n1 = f . (o _ (n1,1)) & ... & the one-to-one onto FinSequence of F . n1 = f . (o _ (n1,(len (o . n1)))) by A3;
A7: the one-to-one onto FinSequence of F . n2 = f . (o _ (n2,1)) & ... & the one-to-one onto FinSequence of F . n2 = f . (o _ (n2,(len (o . n2)))) by A3;
( 1 <= i1 & i1 <= len (o . n1) ) by A5, FINSEQ_3:25;
then A8: the one-to-one onto FinSequence of F . n1 = f . (o _ (n1,i1)) by A6;
A9: ( 1 <= i2 & i2 <= len (o . n2) ) by A5, FINSEQ_3:25;
len o = len C by CARD_1:def 7;
then A10: dom o = dom the one-to-one onto FinSequence of F by FINSEQ_3:29;
A11: n1 in dom o

end;

end;

end;