defpred S_{1}[ 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;

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_{1}[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

$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 S_{1}[m,n]

consider p being FinSequence of NAT such that ex n being Element of NAT st S

let m be Nat; :: thesis: ( m in Seg (len the charact of U1) implies ex n being Element of NAT st S_{1}[m,n] )

assume m in Seg (len the charact of U1) ; :: thesis: ex n being Element of NAT st S_{1}[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: S_{1}[m,n]

thus S_{1}[m,n]
; :: thesis: verum

end;assume m in Seg (len the charact of U1) ; :: thesis: ex n being Element of NAT st S

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: S

thus S

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

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