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);

now

assume {} in rng p ; :: thesis: contradiction
then consider x being set such that
A3: x in dom p and
A4: {} = p . x by FUNCT_1:def 3;
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 q = p as Domain-Sequence by A2, RELAT_1:def 9;
take q ; :: thesis: ( len q = len G & ( for j being Element of dom G holds q . j = the carrier of (G . j) ) )
thus len q = len G by A2, FINSEQ_1:def 3; :: thesis: for j being Element of dom G holds q . j = the carrier of (G . j)
let j be Element of dom G; :: thesis: q . 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 n being Element of dom G st
( n = k & q . k = the carrier of (G . n) ) by A2;
hence q . j = the carrier of (G . j) ; :: thesis: verum