consider F being PartFunc of M,V such that

A1: for c being Element of M holds

( c in dom F iff S_{1}[c] )
and

A2: for c being Element of M st c in dom F holds

F /. c = H_{1}(c)
from PARTFUN2:sch 2();

take F ; :: thesis: ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom F holds

F /. c = (f1 /. c) * (f2 /. c) ) )

thus dom F = (dom f1) /\ (dom f2) by A1, SUBSET_1:3; :: thesis: for c being Element of M st c in dom F holds

F /. c = (f1 /. c) * (f2 /. c)

let c be Element of M; :: thesis: ( c in dom F implies F /. c = (f1 /. c) * (f2 /. c) )

assume c in dom F ; :: thesis: F /. c = (f1 /. c) * (f2 /. c)

hence F /. c = (f1 /. c) * (f2 /. c) by A2; :: thesis: verum

A1: for c being Element of M holds

( c in dom F iff S

A2: for c being Element of M st c in dom F holds

F /. c = H

take F ; :: thesis: ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of M st c in dom F holds

F /. c = (f1 /. c) * (f2 /. c) ) )

thus dom F = (dom f1) /\ (dom f2) by A1, SUBSET_1:3; :: thesis: for c being Element of M st c in dom F holds

F /. c = (f1 /. c) * (f2 /. c)

let c be Element of M; :: thesis: ( c in dom F implies F /. c = (f1 /. c) * (f2 /. c) )

assume c in dom F ; :: thesis: F /. c = (f1 /. c) * (f2 /. c)

hence F /. c = (f1 /. c) * (f2 /. c) by A2; :: thesis: verum