let f be Function; :: thesis: for s, t being Element of product f
for A being set holds s +* (t | A) is Element of product f
let s, t be Element of product f; :: thesis: for A being set holds s +* (t | A) is Element of product f
let A be set ; :: thesis: s +* (t | A) is Element of product f
per cases ( f is non-empty or not f is non-empty ) ;
suppose f is non-empty ; :: thesis: s +* (t | A) is Element of product f
then product f <> {} ;
then A1: t in product f ;
product f c= sproduct f by Th51;
hence s +* (t | A) is Element of product f by A1, Th53, Th65; :: thesis: verum
end;
suppose not f is non-empty ; :: thesis: s +* (t | A) is Element of product f
then {} in rng f ;
then A2: product f = {} by Th26;
t = {} by A2, SUBSET_1:def 1;
then t | A = {} ;
hence s +* (t | A) is Element of product f ; :: thesis: verum
end;
end;