:: deftheorem Def6 defines FinPairUnion NORMFORM:def 6 :
for A being set
for b₂ being BinOp of [:(Fin A),(Fin A):] holds
( b₂ = FinPairUnion A iff for x, y being Element of [:(Fin A),(Fin A):] holds b₂ . (x,y) = x \/ y );