let i, k be Nat; :: thesis: for p being FinSequence of REAL st p has_onlyone_value_in k & i <> k holds
p . i = 0
let p be FinSequence of REAL ; :: thesis: ( p has_onlyone_value_in k & i <> k implies p . i = 0 )
assume that
A1: p has_onlyone_value_in k and
A2: i <> k ; :: thesis: p . i = 0

per cases ( not i in dom p or i in dom p ) ;

suppose not i in dom p ; :: thesis: p . i = 0

hence p . i = 0 by FUNCT_1:def 2; :: thesis: verum

end;

suppose i in dom p ; :: thesis: p . i = 0

hence p . i = 0 by A1, A2; :: thesis: verum

end;

end;