set f = <*2,3,8,24*>;
set g = <*(1 / 2),(1 / 3),(1 / 8),(1 / 24)*>;
<*2,3,8,24*> " = <*(1 / 2),(1 / 3),(1 / 8),(1 / 24)*>

proof

A1: ( len (<*2,3,8,24*> ") = 4 & len <*(1 / 2),(1 / 3),(1 / 8),(1 / 24)*> = 4 ) by CARD_1:def 7;
hence len (<*2,3,8,24*> ") = len <*(1 / 2),(1 / 3),(1 / 8),(1 / 24)*> ; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (<*2,3,8,24*> ") or (<*2,3,8,24*> ") . b₁ = <*(1 / 2),(1 / 3),(1 / 8),(1 / 24)*> . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len (<*2,3,8,24*> ") or (<*2,3,8,24*> ") . k = <*(1 / 2),(1 / 3),(1 / 8),(1 / 24)*> . k )
assume ( 1 <= k & k <= len (<*2,3,8,24*> ") ) ; :: thesis: (<*2,3,8,24*> ") . k = <*(1 / 2),(1 / 3),(1 / 8),(1 / 24)*> . k
then not not k = 1 & ... & not k = 4 by A1;
hence <*(1 / 2),(1 / 3),(1 / 8),(1 / 24)*> . k = (<*2,3,8,24*> . k) "
.= (<*2,3,8,24*> ") . k by VALUED_1:10 ;
:: thesis: verum

end;

hence Sum (<*2,3,8,24*> ") = (((1 / 2) + (1 / 3)) + (1 / 8)) + (1 / 24) by Th20
.= 1 ;
:: according to NUMBER17:def 6 :: thesis: verum