let p be FinSequence; :: thesis: for x being object st p just_once_values x holds
for k being Nat st k in dom p & k <> x .. p holds
p . k <> x
let x be object ; :: thesis: ( p just_once_values x implies for k being Nat st k in dom p & k <> x .. p holds
p . k <> x )
assume A1: p just_once_values x ; :: thesis: for k being Nat st k in dom p & k <> x .. p holds
p . k <> x
let k be Nat; :: thesis: ( k in dom p & k <> x .. p implies p . k <> x )
assume A2: ( k in dom p & k <> x .. p & p . k = x ) ; :: thesis: contradiction
p <- x = x .. p by A1, Th25;
hence contradiction by A1, A2, Def3; :: thesis: verum