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

proof

let i be set ; :: thesis: ( i in dom <*(abs a),(abs b)*> implies (abs <*a,b*>) . i = <*(abs a),(abs b)*> . i )
assume A3: i in dom <*(abs a),(abs b)*> ; :: thesis: (abs <*a,b*>) . i = <*(abs a),(abs b)*> . i
A4: ( <*a,b*> . 1 = a & <*a,b*> . 2 = b ) by FINSEQ_1:61;
A5: ( 1 in {1,2} & 2 in {1,2} ) by TARSKI:def 2;

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

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

hence (abs <*a,b*>) . i = abs a by A1, A4, A5, Th17
.= <*(abs a),(abs b)*> . i by A6, FINSEQ_1:61 ;
:: thesis: verum

end;

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

hence (abs <*a,b*>) . i = abs b by A1, A4, A5, Th17
.= <*(abs a),(abs b)*> . i by A7, FINSEQ_1:61 ;
:: thesis: verum

end;

end;

end;

hence abs <*a,b*> = <*(abs a),(abs b)*> by A1, A2, FUNCT_1:9; :: thesis: verum