let n, i 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:182;
A2: rng (Base_FinSeq n,i) c= REAL ;
A3: for x being set st x in dom (Base_FinSeq n,i) holds
(sqrreal * (Base_FinSeq n,i)) . x = (Base_FinSeq n,i) . x

proof

let x be set ; :: 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:23;
A6: x in Seg (len (Base_FinSeq n,i)) by A4, FINSEQ_1:def 3;
then A7: 1 <= nx by FINSEQ_1:3;
len (Base_FinSeq n,i) = n by MATRIXR2:74;
then A8: nx <= n by A6, FINSEQ_1:3;

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, Th2 ;
hence sqr (Base_FinSeq n,i) = Base_FinSeq n,i by A1, A3, FUNCT_1:9; :: thesis: verum