set f = {[{},{}],[{{}},{{}}]};
{[{},{}],[{{}},{{}}]} is Function-like
proof
let x, y, z be object ; :: according to FUNCT_1:def 1 :: thesis: ( [x,y] in {[{},{}],[{{}},{{}}]} & [x,z] in {[{},{}],[{{}},{{}}]} implies y = z )
assume that
A1: [x,y] in {[{},{}],[{{}},{{}}]} and
A2: [x,z] in {[{},{}],[{{}},{{}}]} ; :: thesis: 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; :: thesis: verum
end;
then reconsider f = {[{},{}],[{{}},{{}}]} as Function ;
take f ; :: thesis: not f is constant
take {} ; :: according to FUNCT_1:def 10 :: thesis: ex y being object st
( {} in dom f & y in dom f & not f . {} = f . y )
take {{}} ; :: thesis: ( {} 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; :: thesis: not f . {} = f . {{}}
then f . {} = {} by A5, Def2;
hence not f . {} = f . {{}} by A4, A6, Def2; :: thesis: verum