let f, F be Function; :: thesis: for A being set st f in product F holds
f | A in product (F | A)
let A be set ; :: thesis: ( f in product F implies f | A in product (F | A) )
assume A1: f in product F ; :: thesis: f | A in product (F | A)
then dom f = dom F by CARD_3:9;
then A2: dom (f | A) = (dom F) /\ A by RELAT_1:61
.= dom (F | A) by RELAT_1:61 ;
for x being object st x in dom (F | A) holds
(f | A) . x in (F | A) . x

proof

let x be object ; :: thesis: ( x in dom (F | A) implies (f | A) . x in (F | A) . x )
assume A3: x in dom (F | A) ; :: thesis: (f | A) . x in (F | A) . x
then x in (dom F) /\ A by RELAT_1:61;
then A4: x in dom F by XBOOLE_0:def 4;
( (F | A) . x = F . x & (f | A) . x = f . x ) by A2, A3, FUNCT_1:47;
hence (f | A) . x in (F | A) . x by A1, A4, CARD_3:9; :: thesis: verum

end;

hence f | A in product (F | A) by A2, CARD_3:9; :: thesis: verum