let f, g be Function; :: according to CARD_3:def 10 :: thesis: ( not f in AddressParts T or not g in AddressParts T or dom f = dom g )
assume that
A1: f in AddressParts T and
A2: g in AddressParts T ; :: thesis: dom f = dom g
A3: ex I being Instruction of st
( f = AddressPart I & InsCode I = T ) by A1;
ex J being Instruction of st
( g = AddressPart J & InsCode J = T ) by A2;
hence dom f = dom g by A3, Def4; :: thesis: verum