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:27
.= {1,2} by FINSEQ_1:2, FINSEQ_1:89 ;
A2: dom <*(abs a),(abs b)*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
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 )
A3: <*a,b*> . 1 = a by FINSEQ_1:44;
A4: <*a,b*> . 2 = b by FINSEQ_1:44;
A5: 2 in {1,2} by TARSKI:def 2;
A6: 1 in {1,2} by TARSKI:def 2;
assume A7: i in dom <*(abs a),(abs b)*> ; :: thesis: (abs <*a,b*>) . i = <*(abs a),(abs b)*> . i

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

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

hence (abs <*a,b*>) . i = abs a by A1, A3, A6, Th17
.= <*(abs a),(abs b)*> . i by A8, FINSEQ_1:44 ;
:: thesis: verum

end;

suppose A9: 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 A9, FINSEQ_1:44 ;
:: thesis: verum

end;

end;

end;

hence abs <*a,b*> = <*(abs a),(abs b)*> by A1, FINSEQ_1:2, FINSEQ_1:89, FUNCT_1:2; :: thesis: verum