let e be Element of product f; :: thesis: e is total
thus dom e = dom f by Th18
.= I by PARTFUN1:def 4 ; :: according to PARTFUN1:def 4 :: thesis: verum