defpred S₁[ Nat, object ] means $2 = len (F . $1);
A1: for k being Nat st k in Seg (len F) holds
ex x being Element of NAT st S₁[k,x] ;
consider IT being FinSequence of NAT such that
A2: ( dom IT = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S₁[k,IT . k] ) ) from FINSEQ_1:sch 5(A1);
take IT ; :: thesis: ( dom IT = dom F & ( for n being Nat st n in dom IT holds
IT . n = len (F . n) ) )
thus dom IT = dom F by A2, FINSEQ_1:def 3; :: thesis: for n being Nat st n in dom IT holds
IT . n = len (F . n)
thus for n being Nat st n in dom IT holds
IT . n = len (F . n) by A2; :: thesis: verum