let I be set ; :: thesis: for f being non-empty I -defined Function
for p being I -defined b₁ -compatible Function ex s being Element of product f st p c= s
let f be non-empty I -defined Function; :: thesis: for p being I -defined f -compatible Function ex s being Element of product f st p c= s
let p be I -defined f -compatible Function; :: thesis: ex s being Element of product f st p c= s
reconsider p = p as Element of sproduct f by Th100;
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