let p be FinSequence; :: thesis: for x being object st x in rng p & ( for k being Nat st k in dom p & k <> x .. p holds
p . k <> x ) holds
p just_once_values x
let x be object ; :: thesis: ( x in rng p & ( for k being Nat st k in dom p & k <> x .. p holds
p . k <> x ) implies p just_once_values x )
assume that
A1: x in rng p and
A2: for k being Nat st k in dom p & k <> x .. p holds
p . k <> x ; :: thesis: p just_once_values x
A3: for z being object st z in dom p & z <> x .. p holds
p . z <> x by A2;
( p . (x .. p) = x & x .. p in dom p ) by A1, Th19, Th20;
hence p just_once_values x by A3, Th7; :: thesis: verum