let i, j be Nat; :: thesis: ( f |^ i = ZeroMap V,V & ( for k being Nat st f |^ k = ZeroMap V,V holds
i <= k ) & f |^ j = ZeroMap V,V & ( for k being Nat st f |^ k = ZeroMap V,V holds
j <= k ) implies i = j )
assume that
A4: ( f |^ i = ZeroMap V,V & ( for k being Nat st f |^ k = ZeroMap V,V holds
i <= k ) ) and
A5: ( f |^ j = ZeroMap V,V & ( for k being Nat st f |^ k = ZeroMap V,V holds
j <= k ) ) ; :: thesis: i = j
( i <= j & j <= i ) by A4, A5;
hence i = j by XXREAL_0:1; :: thesis: verum