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

proof

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;

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