let p be FinSequence; :: thesis: for X being set holds
( p | X is FinSequence iff ex k being Element of NAT st X /\ (dom p) = Seg k )
let X be set ; :: thesis: ( p | X is FinSequence iff ex k being Element of NAT st X /\ (dom p) = Seg k )
thus ( p | X is FinSequence implies ex k being Element of NAT st X /\ (dom p) = Seg k ) :: thesis: ( ex k being Element of NAT st X /\ (dom p) = Seg k implies p | X is FinSequence )
proof
assume p | X is FinSequence ; :: thesis: ex k being Element of NAT st X /\ (dom p) = Seg k
then consider k being Nat such that
A1: dom (p | X) = Seg k by FINSEQ_1:def 2;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
take k ; :: thesis: X /\ (dom p) = Seg k
thus X /\ (dom p) = Seg k by A1, RELAT_1:61; :: thesis: verum
end;
given k being Element of NAT such that A2: X /\ (dom p) = Seg k ; :: thesis: p | X is FinSequence
dom (p | X) = Seg k by A2, RELAT_1:61;
hence p | X is FinSequence by FINSEQ_1:def 2; :: thesis: verum