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

proof

let n be Nat; :: thesis: ( not Sk . n is empty implies for m being Nat st m < n holds
not Sk . m is empty )
assume A1: not Sk . n is empty ; :: thesis: for m being Nat st m < n holds
not Sk . m is empty
n in NAT by ORDINAL1:def 12;
hence for m being Nat st m < n holds
not Sk . m is empty by A1, FUNCOP_1:7; :: thesis: verum

end;

then Sk is lower_non-empty by Def3;
hence ( TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) is lower_non-empty & TriangStr(# Sk, the ManySortedFunction of NatEmbSeq , FuncsSeq Sk #) is strict ) by Def8; :: thesis: verum