let f be non-empty Function; :: thesis: for s, ss being Element of product f
for A being set holds (ss +* (s | A)) | A = s | A
let s, ss be Element of product f; :: thesis: for A being set holds (ss +* (s | A)) | A = s | A
let A be set ; :: thesis: (ss +* (s | A)) | A = s | A
dom s = dom f by Th9
.= dom ss by Th9 ;
then A /\ (dom ss) c= A /\ (dom s) ;
hence (ss +* (s | A)) | A = s | A by FUNCT_4:88; :: thesis: verum