set Sk = NAT --> {};
reconsider Sk = NAT --> {} as ManySortedSet of NAT ;
set A = the ManySortedFunction of NatEmbSeq , FuncsSeq Sk;
take
TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #)
; ( TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) is lower_non-empty & TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) is strict )
for n being Nat st not Sk . n is empty holds
for m being Nat st m < n holds
not Sk . m is empty
by FUNCOP_1:7, ORDINAL1:def 12;
then
Sk is lower_non-empty
;
hence
( TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) is lower_non-empty & TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) is strict )
; verum