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