defpred S₁[ set , set ] means ex j9 being Element of dom g st
( j9 = $1 & $2 = the carrier of (g . j9) );
A1: for j being Nat st j in Seg (len g) holds
ex x being set st S₁[j,x]

proof

let j be Nat; :: thesis: ( j in Seg (len g) implies ex x being set st S₁[j,x] )
assume j in Seg (len g) ; :: thesis: ex x being set st S₁[j,x]
then reconsider j9 = j as Element of dom g by FINSEQ_1:def 3;
take the carrier of (g . j9) ; :: thesis: S₁[j, the carrier of (g . j9)]
thus S₁[j, the carrier of (g . j9)] ; :: thesis: verum

end;

consider p being FinSequence such that
A2: ( dom p = Seg (len g) & ( for j being Nat st j in Seg (len g) holds
S₁[j,p . j] ) ) from FINSEQ_1:sch 1(A1);
p is non-empty

proof

assume {} in rng p ; :: according to RELAT_1:def 9 :: thesis: contradiction
then consider x being set such that
A3: x in dom p and
A4: {} = p . x by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A3;
ex x9 being Element of dom g st
( x9 = x & p . x = the carrier of (g . x9) ) by A2, A3;
hence contradiction by A4; :: thesis: verum

end;

then reconsider p9 = p as Domain-Sequence by A2, FINSEQ_1:def 3;
take p9 ; :: thesis: ( len p9 = len g & ( for j being Element of dom g holds p9 . j = the carrier of (g . j) ) )
thus len p9 = len g by A2, FINSEQ_1:def 3; :: thesis: for j being Element of dom g holds p9 . j = the carrier of (g . j)
let j be Element of dom g; :: thesis: p9 . j = the carrier of (g . j)
reconsider k = j as Element of NAT ;
dom g = Seg (len g) by FINSEQ_1:def 3;
then ex j9 being Element of dom g st
( j9 = k & p9 . k = the carrier of (g . j9) ) by A2;
hence p9 . j = the carrier of (g . j) ; :: thesis: verum