thus
{[0,{},{}]} is J/A-independent
:: thesis: {[0,{},{}]} is homogeneous

assume InsCode I = InsCode J ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

( I = [0,{},{}] & J = [0,{},{}] ) by TARSKI:def 1;

hence dom (JumpPart I) = dom (JumpPart J) ; :: thesis: verum

proof

let I, J be Element of {[0,{},{}]}; :: according to COMPOS_0:def 5 :: thesis: ( InsCode I = InsCode J implies dom (JumpPart I) = dom (JumpPart J) )
let T be InsType of {[0,{},{}]}; :: according to COMPOS_0:def 7 :: thesis: for f1, f2 being natural-valued Function st f1 in JumpParts T & dom f1 = dom f2 holds

for p being object st [T,f1,p] in {[0,{},{}]} holds

[T,f2,p] in {[0,{},{}]}

let f1, f2 be natural-valued Function; :: thesis: ( f1 in JumpParts T & dom f1 = dom f2 implies for p being object st [T,f1,p] in {[0,{},{}]} holds

[T,f2,p] in {[0,{},{}]} )

assume that

A1: f1 in JumpParts T and

A2: dom f1 = dom f2 ; :: thesis: for p being object st [T,f1,p] in {[0,{},{}]} holds

[T,f2,p] in {[0,{},{}]}

let p be object ; :: thesis: ( [T,f1,p] in {[0,{},{}]} implies [T,f2,p] in {[0,{},{}]} )

A3: f1 in {0} by A1, Lm1;

( f1 = 0 & f2 = 0 ) by A3, A2, CARD_3:10;

hence ( [T,f1,p] in {[0,{},{}]} implies [T,f2,p] in {[0,{},{}]} ) ; :: thesis: verum

end;for p being object st [T,f1,p] in {[0,{},{}]} holds

[T,f2,p] in {[0,{},{}]}

let f1, f2 be natural-valued Function; :: thesis: ( f1 in JumpParts T & dom f1 = dom f2 implies for p being object st [T,f1,p] in {[0,{},{}]} holds

[T,f2,p] in {[0,{},{}]} )

assume that

A1: f1 in JumpParts T and

A2: dom f1 = dom f2 ; :: thesis: for p being object st [T,f1,p] in {[0,{},{}]} holds

[T,f2,p] in {[0,{},{}]}

let p be object ; :: thesis: ( [T,f1,p] in {[0,{},{}]} implies [T,f2,p] in {[0,{},{}]} )

A3: f1 in {0} by A1, Lm1;

( f1 = 0 & f2 = 0 ) by A3, A2, CARD_3:10;

hence ( [T,f1,p] in {[0,{},{}]} implies [T,f2,p] in {[0,{},{}]} ) ; :: thesis: verum

assume InsCode I = InsCode J ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

( I = [0,{},{}] & J = [0,{},{}] ) by TARSKI:def 1;

hence dom (JumpPart I) = dom (JumpPart J) ; :: thesis: verum