defpred S_{1}[ set , object ] 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 object st S_{1}[j,x]

A2: ( dom p = Seg (len G) & ( for j being Nat st j in Seg (len G) holds

S_{1}[j,p . j] ) )
from FINSEQ_1:sch 1(A1);

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

( j9 = $1 & $2 = the carrier of (G . j9) );

A1: for j being Nat st j in Seg (len G) holds

ex x being object st S

proof

consider p being FinSequence such that
let j be Nat; :: thesis: ( j in Seg (len G) implies ex x being object st S_{1}[j,x] )

assume j in Seg (len G) ; :: thesis: ex x being object st S_{1}[j,x]

then reconsider j9 = j as Element of dom G by FINSEQ_1:def 3;

take the carrier of (G . j9) ; :: thesis: S_{1}[j, the carrier of (G . j9)]

thus S_{1}[j, the carrier of (G . j9)]
; :: thesis: verum

end;assume j in Seg (len G) ; :: thesis: ex x being object st S

then reconsider j9 = j as Element of dom G by FINSEQ_1:def 3;

take the carrier of (G . j9) ; :: thesis: S

thus S

A2: ( dom p = Seg (len G) & ( for j being Nat st j in Seg (len G) holds

S

now :: thesis: not {} in rng p

then reconsider q = p as Domain-Sequence by A2, RELAT_1:def 9;assume
{} in rng p
; :: thesis: contradiction

then consider x being object 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 consider x being object 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

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