let a, b be Real; :: thesis: sqr <*a,b*> = <*(a ^2 ),(b ^2 )*>
dom sqrreal = REAL by FUNCT_2:def 1;
then A1: rng <*a,b*> c= dom sqrreal ;
A2: dom (sqr <*a,b*>) = dom (sqrreal * <*a,b*>) by RVSUM_1:def 8
.= dom <*a,b*> by A1, RELAT_1:46
.= {1,2} by FINSEQ_1:4, FINSEQ_3:29 ;
A3: dom <*(a ^2 ),(b ^2 )*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
for i being set st i in dom <*(a ^2 ),(b ^2 )*> holds
(sqr <*a,b*>) . i = <*(a ^2 ),(b ^2 )*> . i

proof

let i be set ; :: thesis: ( i in dom <*(a ^2 ),(b ^2 )*> implies (sqr <*a,b*>) . i = <*(a ^2 ),(b ^2 )*> . i )
assume A4: i in dom <*(a ^2 ),(b ^2 )*> ; :: thesis: (sqr <*a,b*>) . i = <*(a ^2 ),(b ^2 )*> . i
A5: ( <*a,b*> . 1 = a & <*a,b*> . 2 = b ) by FINSEQ_1:61;

per cases ( i = 1 or i = 2 ) by A3, A4, TARSKI:def 2;

suppose A6: i = 1 ; :: thesis: (sqr <*a,b*>) . i = <*(a ^2 ),(b ^2 )*> . i

hence (sqr <*a,b*>) . i = a ^2 by A5, VALUED_1:11
.= <*(a ^2 ),(b ^2 )*> . i by A6, FINSEQ_1:61 ;
:: thesis: verum

end;

suppose A7: i = 2 ; :: thesis: (sqr <*a,b*>) . i = <*(a ^2 ),(b ^2 )*> . i

hence (sqr <*a,b*>) . i = b ^2 by A5, VALUED_1:11
.= <*(a ^2 ),(b ^2 )*> . i by A7, FINSEQ_1:61 ;
:: thesis: verum

end;

end;

end;

hence sqr <*a,b*> = <*(a ^2 ),(b ^2 )*> by A2, A3, FUNCT_1:9; :: thesis: verum