let f be non-empty Function; :: thesis: for p being Element of sproduct f ex s being Element of product f st p c= s
let p be Element of sproduct f; :: thesis: ex s being Element of product f st p c= s
set h = the Element of product f;
reconsider s = the Element of product f +* p as Element of product f by Th53;
take s ; :: thesis: p c= s
thus p c= s by FUNCT_4:25; :: thesis: verum