per cases ( not A is empty or A is empty ) ;
suppose not A is empty ; :: thesis: f | A is FinSubsequence-like
then reconsider A9 = A as non empty finite with_non-empty_elements natural-membered set ;
reconsider k = max A9 as Element of NAT by ORDINAL1:def 12;
A1: dom (f | A) c= A by RELAT_1:58;
dom (f | A) c= Seg k
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (f | A) or x in Seg k )
assume A2: x in dom (f | A) ; :: thesis: x in Seg k
then reconsider x9 = x as Nat by A1;
reconsider x9 = x9 as Element of NAT by ORDINAL1:def 12;
( 1 <= x9 & x9 <= k ) by A1, A2, NAT_1:14, XXREAL_2:def 8;
hence x in Seg k ; :: thesis: verum
end;
hence f | A is FinSubsequence-like ; :: thesis: verum
end;
suppose A is empty ; :: thesis: f | A is FinSubsequence-like
hence f | A is FinSubsequence-like ; :: thesis: verum
end;
end;