defpred S1[ 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 S1[j,x]
proof
let j be Nat; :: thesis: ( j in Seg (len G) implies ex x being object st S1[j,x] )
assume j in Seg (len G) ; :: thesis: ex x being object st S1[j,x]
then reconsider j9 = j as Element of dom G by FINSEQ_1:def 3;
take the carrier of (G . j9) ; :: thesis: S1[j, the carrier of (G . j9)]
thus S1[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
S1[j,p . j] ) ) from
now :: thesis: not {} in rng p
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 reconsider q = p as Domain-Sequence by ;
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 ; :: 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