set S = {[0,{},{}],[1,{},{}]};

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

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

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

proof

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

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