defpred S1[ Nat, set ] means for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . \$1 holds
\$2 = arity h;
A1: now :: thesis: for m being Nat st m in Seg (len the charact of U1) holds
ex n being Element of NAT st S1[m,n]
let m be Nat; :: thesis: ( m in Seg (len the charact of U1) implies ex n being Element of NAT st S1[m,n] )
assume m in Seg (len the charact of U1) ; :: thesis: ex n being Element of NAT st S1[m,n]
then m in dom the charact of U1 by FINSEQ_1:def 3;
then reconsider H = the charact of U1 . m as non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 ;
reconsider n = arity H as Element of NAT ;
take n = n; :: thesis: S1[m,n]
thus S1[m,n] ; :: thesis: verum
end;
consider p being FinSequence of NAT such that
A2: dom p = Seg (len the charact of U1) and
A3: for m being Nat st m in Seg (len the charact of U1) holds
S1[m,p . m] from take p ; :: thesis: ( len p = len the charact of U1 & ( for n being Nat st n in dom p holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
p . n = arity h ) )

thus len p = len the charact of U1 by ; :: thesis: for n being Nat st n in dom p holds
for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
p . n = arity h

let n be Nat; :: thesis: ( n in dom p implies for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
p . n = arity h )

assume A4: n in dom p ; :: thesis: for h being non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1 st h = the charact of U1 . n holds
p . n = arity h

let h be non empty homogeneous PartFunc of ( the carrier of U1 *), the carrier of U1; :: thesis: ( h = the charact of U1 . n implies p . n = arity h )
assume h = the charact of U1 . n ; :: thesis: p . n = arity h
hence p . n = arity h by A2, A3, A4; :: thesis: verum