defpred S₁[ 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

let m be Nat; :: thesis: ( m in Seg (len the charact of U1) implies ex n being Element of NAT st S₁[m,n] )
assume m in Seg (len the charact of U1) ; :: thesis: ex n being Element of NAT st S₁[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 by Th5;
reconsider n = arity H as Element of NAT ;
take n = n; :: thesis: S₁[m,n]
thus S₁[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
S₁[m,p . m] from FINSEQ_1:sch 5(A1);
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 A2, FINSEQ_1:def 3; :: 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