set f = <*15,20,12*>;
set h = <*15,20,12*> | 2;
set g = ((<*15,20,12*> | 2) ") ^2 ;
((<*15,20,12*> | 2) ") ^2 = <*(1 / (15 ^2)),(1 / (20 ^2))*>

proof

dom (((<*15,20,12*> | 2) ") ^2) = (dom ((<*15,20,12*> | 2) ")) /\ (dom ((<*15,20,12*> | 2) ")) by VALUED_1:def 4;
then A1: len (((<*15,20,12*> | 2) ") ^2) = len (<*15,20,12*> | 2) by VALUED_1:def 7, FINSEQ_3:29;
len <*15,20,12*> = 3 by FINSEQ_1:45;
then A2: len (<*15,20,12*> | 2) = 2 by FINSEQ_1:59;
hence len (((<*15,20,12*> | 2) ") ^2) = len <*(1 / (15 ^2)),(1 / (20 ^2))*> by A1, FINSEQ_1:44; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (((<*15,20,12*> | 2) ") ^2) or (((<*15,20,12*> | 2) ") ^2) . b₁ = <*(1 / (15 ^2)),(1 / (20 ^2))*> . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len (((<*15,20,12*> | 2) ") ^2) or (((<*15,20,12*> | 2) ") ^2) . k = <*(1 / (15 ^2)),(1 / (20 ^2))*> . k )
assume that
1 <= k and
A3: k <= len (((<*15,20,12*> | 2) ") ^2) ; :: thesis: (((<*15,20,12*> | 2) ") ^2) . k = <*(1 / (15 ^2)),(1 / (20 ^2))*> . k
A4: (((<*15,20,12*> | 2) ") ^2) . k = (((<*15,20,12*> | 2) ") . k) ^2 by VALUED_1:11;
A5: ((<*15,20,12*> | 2) ") . k = ((<*15,20,12*> | 2) . k) " by VALUED_1:10;
not not k = 0 & ... & not k = 2 by A1, A2, A3;
hence (((<*15,20,12*> | 2) ") ^2) . k = <*(1 / (15 ^2)),(1 / (20 ^2))*> . k by A4, A5; :: thesis: verum

end;

then Sum (((<*15,20,12*> | 2) ") ^2) = (1 / (15 ^2)) + (1 / (20 ^2)) by RVSUM_1:77;
hence <*15,20,12*> is a_solution_of_Sierp168 ; :: thesis: verum