set S = {[0,{},{}],[1,{},{}]};
thus {[0,{},{}],[1,{},{}]} is J/A-independent :: thesis: {[0,{},{}],[1,{},{}]} is homogeneous

proof

let T be InsType of {[0,{},{}],[1,{},{}]}; :: 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,{},{}],[1,{},{}]} holds
[T,f2,p] in {[0,{},{}],[1,{},{}]}
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,{},{}],[1,{},{}]} holds
[T,f2,p] in {[0,{},{}],[1,{},{}]} )
assume that
A1: f1 in JumpParts T and
A2: dom f1 = dom f2 ; :: thesis: for p being object st [T,f1,p] in {[0,{},{}],[1,{},{}]} holds
[T,f2,p] in {[0,{},{}],[1,{},{}]}
let p be object ; :: thesis: ( [T,f1,p] in {[0,{},{}],[1,{},{}]} implies [T,f2,p] in {[0,{},{}],[1,{},{}]} )
A3: f1 in {0} by A1, Lm4;
( f1 = 0 & f2 = 0 ) by A3, A2, CARD_3:10;
hence ( [T,f1,p] in {[0,{},{}],[1,{},{}]} implies [T,f2,p] in {[0,{},{}],[1,{},{}]} ) ; :: thesis: verum

end;

let I, J be Element of {[0,{},{}],[1,{},{}]}; :: 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)
( JumpPart I = {} & JumpPart J = {} ) by Th8;
hence dom (JumpPart I) = dom (JumpPart J) ; :: thesis: verum