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

proof

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

end;

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