let i, n be Nat; :: thesis: sqr (Base_FinSeq (n,i)) = Base_FinSeq (n,i)
A1: dom (sqrreal * (Base_FinSeq (n,i))) = (Base_FinSeq (n,i)) " (dom sqrreal) by RELAT_1:147;
A2: rng (Base_FinSeq (n,i)) c= REAL ;
A3: for x being object st x in dom (Base_FinSeq (n,i)) holds
(sqrreal * (Base_FinSeq (n,i))) . x = (Base_FinSeq (n,i)) . x

proof

let x be object ; :: thesis: ( x in dom (Base_FinSeq (n,i)) implies (sqrreal * (Base_FinSeq (n,i))) . x = (Base_FinSeq (n,i)) . x )
assume A4: x in dom (Base_FinSeq (n,i)) ; :: thesis: (sqrreal * (Base_FinSeq (n,i))) . x = (Base_FinSeq (n,i)) . x
then reconsider nx = x as Element of NAT ;
A5: (sqrreal * (Base_FinSeq (n,i))) . x = sqrreal . ((Base_FinSeq (n,i)) . x) by A4, FUNCT_1:13;
A6: x in Seg (len (Base_FinSeq (n,i))) by A4, FINSEQ_1:def 3;
then A7: 1 <= nx by FINSEQ_1:1;
len (Base_FinSeq (n,i)) = n by MATRIXR2:74;
then A8: nx <= n by A6, FINSEQ_1:1;

per cases ( nx = i or nx <> i ) ;

suppose A9: nx = i ; :: thesis: (sqrreal * (Base_FinSeq (n,i))) . x = (Base_FinSeq (n,i)) . x

hence (sqrreal * (Base_FinSeq (n,i))) . x = sqrreal . 1 by A7, A8, A5, MATRIXR2:75
.= 1 ^2 by RVSUM_1:def 2
.= (Base_FinSeq (n,i)) . x by A7, A8, A9, MATRIXR2:75 ;
:: thesis: verum

end;

suppose A10: nx <> i ; :: thesis: (sqrreal * (Base_FinSeq (n,i))) . x = (Base_FinSeq (n,i)) . x

hence (sqrreal * (Base_FinSeq (n,i))) . x = sqrreal . 0 by A7, A8, A5, MATRIXR2:76
.= 0 ^2 by RVSUM_1:def 2
.= (Base_FinSeq (n,i)) . x by A7, A8, A10, MATRIXR2:76 ;
:: thesis: verum

end;

end;

end;

(Base_FinSeq (n,i)) " (dom sqrreal) = (Base_FinSeq (n,i)) " REAL by FUNCT_2:def 1
.= dom (Base_FinSeq (n,i)) by A2, Th1 ;
hence sqr (Base_FinSeq (n,i)) = Base_FinSeq (n,i) by A1, A3, FUNCT_1:2; :: thesis: verum