let p be FinSequence; :: thesis: for x being object st p just_once_values x holds
p <- x = x .. p
let x be object ; :: 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 Th5;
then ( x .. p in dom p & p . (x .. p) = x ) by Th19, Th20;
hence p <- x = x .. p by A1, Def3; :: thesis: verum