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 <*(a ^2),(b ^2)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
A3: for i being object st i in dom <*(a ^2),(b ^2)*> holds
(sqr <*a,b*>) . i = <*(a ^2),(b ^2)*> . i
proof
let i be object ; :: thesis: ( i in dom <*(a ^2),(b ^2)*> implies (sqr <*a,b*>) . i = <*(a ^2),(b ^2)*> . i )
A4: <*a,b*> . 1 = a by FINSEQ_1:44;
A5: <*a,b*> . 2 = b by FINSEQ_1:44;
assume A6: i in dom <*(a ^2),(b ^2)*> ; :: thesis: (sqr <*a,b*>) . i = <*(a ^2),(b ^2)*> . i
per cases ( i = 1 or i = 2 ) by A2, A6, TARSKI:def 2;
suppose A7: i = 1 ; :: thesis: (sqr <*a,b*>) . i = <*(a ^2),(b ^2)*> . i
hence (sqr <*a,b*>) . i = a ^2 by A4, VALUED_1:11
.= <*(a ^2),(b ^2)*> . i by A7, FINSEQ_1:44 ;
:: thesis: verum
end;
suppose A8: 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 A8, FINSEQ_1:44 ;
:: thesis: verum
end;
end;
end;
dom (sqr <*a,b*>) = dom (sqrreal * <*a,b*>) by RVSUM_1:def 8
.= dom <*a,b*> by A1, RELAT_1:27
.= {1,2} by FINSEQ_1:2, FINSEQ_1:89 ;
hence sqr <*a,b*> = <*(a ^2),(b ^2)*> by A3, FINSEQ_1:2, FINSEQ_1:89, FUNCT_1:2; :: thesis: verum