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