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

proof

dom (((<*1,1*> | 1) ") ^2) = (dom ((<*1,1*> | 1) ")) /\ (dom ((<*1,1*> | 1) ")) by VALUED_1:def 4;
then A1: len (((<*1,1*> | 1) ") ^2) = len (<*1,1*> | 1) by VALUED_1:def 7, FINSEQ_3:29;
hence len (((<*1,1*> | 1) ") ^2) = len <*1*> ; :: according to FINSEQ_1:def 18 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not b₁ <= len (((<*1,1*> | 1) ") ^2) or (((<*1,1*> | 1) ") ^2) . b₁ = <*1*> . b₁ )
let k be Nat; :: thesis: ( not 1 <= k or not k <= len (((<*1,1*> | 1) ") ^2) or (((<*1,1*> | 1) ") ^2) . k = <*1*> . k )
assume ( 1 <= k & k <= len (((<*1,1*> | 1) ") ^2) ) ; :: thesis: (((<*1,1*> | 1) ") ^2) . k = <*1*> . k
then A2: k = 1 by A1, XXREAL_0:1;
((<*1,1*> | 1) ") . 1 = ((<*1,1*> | 1) . 1) " ;
hence <*1*> . k = (((<*1,1*> | 1) ") . 1) ^2 by A2
.= (((<*1,1*> | 1) ") ^2) . k by A2, VALUED_1:11 ;
:: thesis: verum

end;

hence <*1,1*> is a_solution_of_Sierp168 ; :: thesis: verum