let S be set ; :: thesis: ( S is product-like implies ( S is functional & S is with_common_domain ) )
given f being Function such that A1: S = product f ; :: according to CARD_3:def 13 :: thesis: ( S is functional & S is with_common_domain )
thus S is functional by A1; :: thesis: S is with_common_domain
let h, g be Function; :: according to CARD_3:def 10 :: thesis: ( h in S & g in S implies dom h = dom g )
assume that
A2: h in S and
A3: g in S ; :: thesis: dom h = dom g
thus dom h = dom f by A1, A2, Th9
.= dom g by A1, A3, Th9 ; :: thesis: verum