let n, i be Nat; :: thesis: sqr (Base_FinSeq n,i) = Base_FinSeq n,i
A2: dom (sqrreal * (Base_FinSeq n,i)) = (Base_FinSeq n,i) " (dom sqrreal ) by RELAT_1:182;
A3: rng (Base_FinSeq n,i) c= REAL ;
A4: (Base_FinSeq n,i) " (dom sqrreal ) = (Base_FinSeq n,i) " REAL by FUNCT_2:def 1
.= dom (Base_FinSeq n,i) by Th2, 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 A5: x in dom (Base_FinSeq n,i) ; :: thesis: (sqrreal * (Base_FinSeq n,i)) . x = (Base_FinSeq n,i) . x
then A6: x in Seg (len (Base_FinSeq n,i)) by FINSEQ_1:def 3;
reconsider nx = x as Element of NAT by A5;
len (Base_FinSeq n,i) = n by MATRIXR2:74;
then A7: ( 1 <= nx & nx <= n ) by A6, FINSEQ_1:3;
A8: (sqrreal * (Base_FinSeq n,i)) . x = sqrreal . ((Base_FinSeq n,i) . x) by A5, FUNCT_1:23;

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, MATRIXR2:75
.= 1 ^2 by RVSUM_1:def 2
.= (Base_FinSeq n,i) . x by A7, 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, MATRIXR2:76
.= 0 ^2 by RVSUM_1:def 2
.= (Base_FinSeq n,i) . x by A7, A10, MATRIXR2:76 ;
:: thesis: verum

end;

end;

end;

hence sqr (Base_FinSeq n,i) = Base_FinSeq n,i by A2, A4, FUNCT_1:9; :: thesis: verum