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 #) ; :: thesis: ( 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 ) ; :: thesis: verum