let R, S be non empty doubleLoopStr ; :: thesis: for f being Function of R,S
for x being Element of R st x in ker f holds
f . x = 0. S
let f be Function of R,S; :: thesis: for x being Element of R st x in ker f holds
f . x = 0. S
let x be Element of R; :: thesis: ( x in ker f implies f . x = 0. S )
assume x in ker f ; :: thesis: f . x = 0. S
then ex y being Element of R st
( y = x & f . y = 0. S ) ;
hence f . x = 0. S ; :: thesis: verum