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