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 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 <*|.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, FINSEQ_1:44 ;
:: 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, FINSEQ_1:44 ;
:: thesis: verum
end;
end;
end;
hence abs <*a,b*> = <*|.a.|,|.b.|*> by A1, FINSEQ_1:2, FINSEQ_1:89, FUNCT_1:2; :: thesis: verum