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 ( not rng g is empty & rng g = the carrier of (Image g) ) by RELAT_1:65, YELLOW_0:def 15;
then consider l being set such that
A1: l in dom g and
A2: s = g . l by FUNCT_1:def 5;
reconsider l = l as Element of L1 by A1;
take l ; :: thesis: g . l = s
thus g . l = s by A2; :: thesis: verum