let a, b be Real; :: thesis: abs <*a,b*> = <*|.a.|,|.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 <*|.a.|,|.b.|*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89;
reconsider a = a, b = b as Element of REAL by XREAL_0:def 1;
for i being object st i in dom <*|.a.|,|.b.|*> holds
(abs <*a,b*>) . i = <*|.a.|,|.b.|*> . i

proof

let i be object ; :: thesis: ( i in dom <*|.a.|,|.b.|*> implies (abs <*a,b*>) . i = <*|.a.|,|.b.|*> . i )
A3: <*a,b*> . 1 = a ;
A4: <*a,b*> . 2 = b ;
A5: 2 in {1,2} by TARSKI:def 2;
A6: 1 in {1,2} by TARSKI:def 2;
assume A7: i in dom <*|.a.|,|.b.|*> ; :: thesis: (abs <*a,b*>) . i = <*|.a.|,|.b.|*> . i

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

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

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

end;

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

hence (abs <*a,b*>) . i = |.b.| by A1, A4, A5, Th11
.= <*|.a.|,|.b.|*> . i by A9 ;
:: thesis: verum

end;

end;

end;

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