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

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

A2: now

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

end;

now

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

now

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

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

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

end;

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

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

end;

end;

end;

hence p in g ; :: 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

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

A9: now

assume p in dom g ; :: thesis: ( p = o or p = q )
then [p,(g . p)] in g by FUNCT_1:8;
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 ZFMISC_1:33; :: thesis: verum

end;

now

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

now

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:8; :: 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:8; :: thesis: verum

end;

end;

end;

hence p in dom g ; :: 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