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

take 2 ; :: thesis: ( 1 in dom f & 2 in dom f & not f . 1 = f . 2 )
A4: [2,2] in f by TARSKI:def 2;
A5: [1,1] in f by TARSKI:def 2;
hence A6: ( 1 in dom f & 2 in dom f ) by A4, RELAT_1:def 4; :: thesis: not f . 1 = f . 2
then f . 1 = 1 by A5, Def4;
hence not f . 1 = f . 2 by A4, A6, Def4; :: thesis: verum