let f be FinSequence of REAL ; :: thesis: ( f = |.p.| iff ( len f = len p & ( for n being Nat st n in dom p holds
f . n = |.(p . n).| ) ) )

hereby :: thesis: ( len f = len p & ( for n being Nat st n in dom p holds
f . n = |.(p . n).| ) implies f = |.p.| )

assume A1: f = |.p.| ; :: thesis: ( len f = len p & ( for n being Nat st n in dom p holds
f . n = |.(p . n).| ) )
dom |.p.| = dom p by VALUED_1:def 11;
hence len f = len p by A1, FINSEQ_3:29; :: thesis: for n being Nat st n in dom p holds
f . n = |.(p . n).|
let n be Nat; :: thesis: ( n in dom p implies f . n = |.(p . n).| )
assume n in dom p ; :: thesis: f . n = |.(p . n).|
thus f . n = |.(p . n).| by A1, VALUED_1:18; :: thesis: verum

end;

assume that
A1: len f = len p and
A2: for n being Nat st n in dom p holds
f . n = |.(p . n).| ; :: thesis: f = |.p.|
A3: dom f = dom p by A1, FINSEQ_3:29;
then for c being object st c in dom f holds
f . c = |.(p . c).| by A2;
hence f = |.p.| by A3, VALUED_1:def 11; :: thesis: verum