let p be FinSequence; :: thesis: for x being set 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 set ; :: 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: ( p . (x .. p) = x & x .. p in dom p ) by A1, Th29, Th30;
for z being set st z in dom p & z <> x .. p holds
p . z <> x by A2;
hence p just_once_values x by A3, Th9; :: thesis: verum