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

proof

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

end;

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