let I be set ; :: thesis: for f being non-empty I -defined Function
for p being I -defined b₁ -compatible Function holds p in sproduct f
let f be non-empty I -defined Function; :: thesis: for p being I -defined f -compatible Function holds p in sproduct f
let p be I -defined f -compatible Function; :: thesis: p in sproduct f
A1: dom p c= dom f by FUNCT_1:105;
for x being object st x in dom p holds
p . x in f . x by FUNCT_1:def 14;
hence p in sproduct f by A1, Def9; :: thesis: verum