let s be Real; :: thesis: abs <*s*> = <*(abs s)*>
rng <*s*> c= dom absreal

proof

let x be set ; :: 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 <*(abs s)*> = 1 by FINSEQ_1:39;
for j being Nat st 1 <= j & j <= len <*(abs s)*> holds
<*(abs s)*> . j = (abs <*s*>) . j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= len <*(abs s)*> implies <*(abs 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 <*(abs s)*> ) ; :: thesis: <*(abs s)*> . j = (abs <*s*>) . j
then A5: j = 1 by A3, XXREAL_0:1;
then <*(abs s)*> . j = abs s by FINSEQ_1:40;
hence <*(abs s)*> . j = (abs <*s*>) . j by A5, A4, VALUED_1:18; :: thesis: verum

end;

hence abs <*s*> = <*(abs s)*> by A2, A3, FINSEQ_1:14; :: thesis: verum