let p be FinSequence; :: thesis: for x being set st p just_once_values x holds
p <- x = x .. p
let x be set ; :: thesis: ( p just_once_values x implies p <- x = x .. p )
assume A1: p just_once_values x ; :: thesis: p <- x = x .. p
then ( p <- x in dom p & x in rng p ) by Def3, Th7;
then ( p <- x in dom p & x .. p in dom p & p . (x .. p) = x & p . (p <- x) = x ) by A1, Def3, Th29, Th30;
hence p <- x = x .. p by A1, Def3; :: thesis: verum