let f be Function; :: thesis: for y being object st f just_once_values y holds
f " {y} = {(f <- y)}
let y be object ; :: thesis: ( f just_once_values y implies f " {y} = {(f <- y)} )
assume A1: f just_once_values y ; :: thesis: f " {y} = {(f <- y)}
then consider x being object such that
A2: {x} = f " {y} by Th6;
A3: x in f " {y} by A2, ZFMISC_1:31;
then f . x in {y} by FUNCT_1:def 7;
then A4: f . x = y by TARSKI:def 1;
x in dom f by A3, FUNCT_1:def 7;
hence f " {y} = {(f <- y)} by A1, A2, A4, Def3; :: thesis: verum