consider F being PartFunc of C,the carrier of V such that
A1: for c being Element of C holds
( c in dom F iff S₁[c] ) and
A2: for c being Element of C st c in dom F holds
F /. c = H₁(c) from PARTFUN2:sch 2();
take F ; :: thesis: ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds
F /. c = (f1 . c) * (f2 /. c) ) )
thus dom F = (dom f1) /\ (dom f2) by A1, SUBSET_1:8; :: thesis: for c being Element of C st c in dom F holds
F /. c = (f1 . c) * (f2 /. c)
let c be Element of C; :: 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