let a, b be non zero Nat; :: thesis: ( a,b are_coprime implies card (support (pfexp (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b))) )
assume A1: a,b are_coprime ; :: thesis: card (support (pfexp (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b)))
support (pfexp (a * b)) = (support (pfexp a)) \/ (support (pfexp b)) by Th46;
hence card (support (pfexp (a * b))) = (card (support (pfexp a))) + (card (support (pfexp b))) by A1, Th44, CARD_2:40; :: thesis: verum