let s be Real; :: thesis: abs <*s*> = <*|.s.|*>
reconsider s = s as Element of REAL by XREAL_0:def 1;
rng <*s*> c= dom absreal
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng <*s*> or x in dom absreal )
assume x in rng <*s*> ; :: thesis: x in dom absreal
then x in {s} by FINSEQ_1:38;
then A1: x = s by TARSKI:def 1;
dom absreal = REAL by FUNCT_2:def 1;
hence x in dom absreal by A1; :: thesis: verum
end;
then dom <*s*> = dom (absreal * <*s*>) by RELAT_1:27;
then Seg 1 = dom (abs <*s*>) by FINSEQ_1:def 8;
then A2: len (abs <*s*>) = 1 by FINSEQ_1:def 3;
A3: len <*|.s.|*> = 1 by FINSEQ_1:39;
for j being Nat st 1 <= j & j <= len <*|.s.|*> holds
<*|.s.|*> . j = (abs <*s*>) . j
proof
let j be Nat; :: thesis: ( 1 <= j & j <= len <*|.s.|*> implies <*|.s.|*> . j = (abs <*s*>) . j )
A4: ( <*s*> . 1 = s & <*s*> is Element of REAL 1 ) by FINSEQ_1:40, FINSEQ_2:98;
assume ( 1 <= j & j <= len <*|.s.|*> ) ; :: thesis: <*|.s.|*> . j = (abs <*s*>) . j
then A5: j = 1 by A3, XXREAL_0:1;
then <*|.s.|*> . j = |.s.| by FINSEQ_1:40;
hence <*|.s.|*> . j = (abs <*s*>) . j by A5, A4, VALUED_1:18; :: thesis: verum
end;
hence abs <*s*> = <*|.s.|*> by A2, A3, FINSEQ_1:14; :: thesis: verum