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 x in rng p by Th7;
then ( x .. p in dom p & p . (x .. p) = x ) by Th29, Th30;
hence p <- x = x .. p by A1, Def3; :: thesis: verum