let f be sequence of INT.Ring; :: thesis: ( f = |.p.| iff for n being Nat holds f . n = |.(p . n).| )
thus ( f = |.p.| implies for n being Nat holds f . n = |.(p . n).| ) by VALUED_1:18; :: thesis: ( ( for n being Nat holds f . n = |.(p . n).| ) implies f = |.p.| )
assume A2: for n being Nat holds f . n = |.(p . n).| ; :: thesis: f = |.p.|
thus dom f = dom |.p.| by A1, FUNCT_2:def 1; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom f or f . b₁ = |.p.| . b₁ )
let x be object ; :: thesis: ( not x in dom f or f . x = |.p.| . x )
assume x in dom f ; :: thesis: f . x = |.p.| . x
hence f . x = |.(p . x).| by A2
.= |.p.| . x by VALUED_1:18 ;
:: thesis: verum