let S be set ; :: thesis: for s being FinSequence of S
for A being Subset of (dom s) holds
( len (extract (s,A)) = card A & ( for i being Nat st i in dom (extract (s,A)) holds
(extract (s,A)) . i = s . ((canFS A) . i) ) )
let s be FinSequence of S; :: thesis: for A being Subset of (dom s) holds
( len (extract (s,A)) = card A & ( for i being Nat st i in dom (extract (s,A)) holds
(extract (s,A)) . i = s . ((canFS A) . i) ) )
let A be Subset of (dom s); :: thesis: ( len (extract (s,A)) = card A & ( for i being Nat st i in dom (extract (s,A)) holds
(extract (s,A)) . i = s . ((canFS A) . i) ) )
rng (canFS A) c= A by FINSEQ_1:def 4;
then len (extract (s,A)) = len (canFS A) by FINSEQ_2:29, XBOOLE_1:1
.= card A by FINSEQ_1:93 ;
hence ( len (extract (s,A)) = card A & ( for i being Nat st i in dom (extract (s,A)) holds
(extract (s,A)) . i = s . ((canFS A) . i) ) ) by FUNCT_1:12; :: thesis: verum