set f = {[{},{}],[{{}},{{}}]};
{[{},{}],[{{}},{{}}]} is Function-like
proof
let x,
y,
z be
object ;
FUNCT_1:def 1 ( [x,y] in {[{},{}],[{{}},{{}}]} & [x,z] in {[{},{}],[{{}},{{}}]} implies y = z )
assume that A1:
[x,y] in {[{},{}],[{{}},{{}}]}
and A2:
[x,z] in {[{},{}],[{{}},{{}}]}
;
y = z
(
[x,y] = [{},{}] or
[x,y] = [{{}},{{}}] )
by A1, TARSKI:def 2;
then A3:
( (
x = {} &
y = {} ) or (
x = {{}} &
y = {{}} ) )
by XTUPLE_0:1;
(
[x,z] = [{},{}] or
[x,z] = [{{}},{{}}] )
by A2, TARSKI:def 2;
hence
y = z
by A3, XTUPLE_0:1;
verum
end;
then reconsider f = {[{},{}],[{{}},{{}}]} as Function ;
take
f
; not f is constant
take
{}
; FUNCT_1:def 10 ex y being object st
( {} in dom f & y in dom f & not f . {} = f . y )
take
{{}}
; ( {} in dom f & {{}} in dom f & not f . {} = f . {{}} )
A4:
[{{}},{{}}] in f
by TARSKI:def 2;
A5:
[{},{}] in f
by TARSKI:def 2;
hence A6:
( {} in dom f & {{}} in dom f )
by A4, XTUPLE_0:def 12; not f . {} = f . {{}}
then
f . {} = {}
by A5, Def2;
hence
not f . {} = f . {{}}
by A4, A6, Def2; verum