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;
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
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