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 ( 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 ) ) ; :: thesis: i = j
then ( i <= j & j <= i ) ;
hence i = j by XXREAL_0:1; :: thesis: verum