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:55;
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:46;
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:56;
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 )
assume ( 1 <= j & j <= len <*(abs s)*> ) ; :: thesis: <*(abs s)*> . j = (abs <*s*>) . j
then A4: j = 1 by A3, XXREAL_0:1;
then A5: <*(abs s)*> . j = abs s by FINSEQ_1:57;
A6: <*s*> . 1 = s by FINSEQ_1:57;
<*s*> in 1 -tuples_on REAL by FINSEQ_2:118;
then <*s*> is Element of REAL 1 ;
hence <*(abs s)*> . j = (abs <*s*>) . j by A4, A5, A6, EUCLID:6; :: thesis: verum

end;

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