let L1, L2 be non empty RelStr ; :: thesis: for f being Function of L1,L2
for y being Element of (Image f) ex x being Element of L1 st f . x = y
let g be Function of L1,L2; :: thesis: for y being Element of (Image g) ex x being Element of L1 st g . x = y
let s be Element of (Image g); :: thesis: ex x being Element of L1 st g . x = s
dom g = the carrier of L1 by FUNCT_2:def 1;
then A1: not rng g is empty by RELAT_1:42;
rng g = the carrier of (Image g) by YELLOW_0:def 15;
then consider l being object such that
A2: l in dom g and
A3: s = g . l by A1, FUNCT_1:def 3;
reconsider l = l as Element of L1 by A2;
take l ; :: thesis: g . l = s
thus g . l = s by A3; :: thesis: verum