let X be set ; :: thesis: for F being FinSequence of X
for i being Nat st i in dom F holds
( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i )
let F be FinSequence of X; :: thesis: for i being Nat st i in dom F holds
( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i )
let i be Nat; :: thesis: ( i in dom F implies ( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i ) )
assume A1: i in dom F ; :: thesis: ( F . i c= union (rng F) & (F . i) /\ (union (rng F)) = F . i )
hence F . i c= union (rng F) by FUNCT_1:3, ZFMISC_1:74; :: thesis: (F . i) /\ (union (rng F)) = F . i
F . i in rng F by A1, FUNCT_1:3;
hence (F . i) /\ (union (rng F)) = F . i by XBOOLE_1:28, ZFMISC_1:74; :: thesis: verum