let o, q be set ; :: thesis: for g being Function holds
( dom g = {o,q} iff g = {[o,(g . o)],[q,(g . q)]} )
let g be Function; :: thesis: ( dom g = {o,q} iff g = {[o,(g . o)],[q,(g . q)]} )

hereby :: thesis: ( g = {[o,(g . o)],[q,(g . q)]} implies dom g = {o,q} )

assume A1: dom g = {o,q} ; :: thesis: g = {[o,(g . o)],[q,(g . q)]}

now :: thesis: for p being object holds
( p in g iff ( p = [o,(g . o)] or p = [q,(g . q)] ) )

let p be object ; :: thesis: ( p in g iff ( p = [o,(g . o)] or p = [q,(g . q)] ) )

A2: now :: thesis: ( ( p = [o,(g . o)] or p = [q,(g . q)] ) implies p in g )

assume A3: ( p = [o,(g . o)] or p = [q,(g . q)] ) ; :: thesis: p in g

now :: thesis: p in g

per cases ( p = [o,(g . o)] or p = [q,(g . q)] ) by A3;

suppose A4: p = [o,(g . o)] ; :: thesis: p in g

o in dom g by A1, TARSKI:def 2;
hence p in g by A4, FUNCT_1:1; :: thesis: verum

end;

suppose A5: p = [q,(g . q)] ; :: thesis: p in g

q in dom g by A1, TARSKI:def 2;
hence p in g by A5, FUNCT_1:1; :: thesis: verum

end;

end;

end;

hence p in g ; :: thesis: verum

end;

now :: thesis: ( not p in g or p = [o,(g . o)] or p = [q,(g . q)] )

assume A6: p in g ; :: thesis: ( p = [o,(g . o)] or p = [q,(g . q)] )
then consider r, s being object such that
A7: p = [r,s] by RELAT_1:def 1;
r in dom g by A6, A7, FUNCT_1:1;
then ( r = o or r = q ) by A1, TARSKI:def 2;
hence ( p = [o,(g . o)] or p = [q,(g . q)] ) by A6, A7, FUNCT_1:1; :: thesis: verum

end;

hence ( p in g iff ( p = [o,(g . o)] or p = [q,(g . q)] ) ) by A2; :: thesis: verum

end;

hence g = {[o,(g . o)],[q,(g . q)]} by TARSKI:def 2; :: thesis: verum

end;

assume A8: g = {[o,(g . o)],[q,(g . q)]} ; :: thesis: dom g = {o,q}

now :: thesis: for p being object holds
( p in dom g iff ( p = o or p = q ) )

let p be object ; :: thesis: ( p in dom g iff ( p = o or p = q ) )

A9: now :: thesis: ( ( p = o or p = q ) implies p in dom g )

assume A10: ( p = o or p = q ) ; :: thesis: p in dom g

now :: thesis: p in dom g

per cases ( p = o or p = q ) by A10;

suppose p = o ; :: thesis: p in dom g

then [p,(g . p)] in g by A8, TARSKI:def 2;
hence p in dom g by FUNCT_1:1; :: thesis: verum

end;

suppose p = q ; :: thesis: p in dom g

then [p,(g . p)] in g by A8, TARSKI:def 2;
hence p in dom g by FUNCT_1:1; :: thesis: verum

end;

end;

end;

hence p in dom g ; :: thesis: verum

end;

now :: thesis: ( not p in dom g or p = o or p = q )

assume p in dom g ; :: thesis: ( p = o or p = q )
then [p,(g . p)] in g by FUNCT_1:1;
then ( [p,(g . p)] = [o,(g . o)] or [p,(g . p)] = [q,(g . q)] ) by A8, TARSKI:def 2;
hence ( p = o or p = q ) by XTUPLE_0:1; :: thesis: verum

end;

hence ( p in dom g iff ( p = o or p = q ) ) by A9; :: thesis: verum

end;

hence dom g = {o,q} by TARSKI:def 2; :: thesis: verum