let A be set ; :: thesis: [({}. A),({}. A)] is_a_unity_wrt FinPairUnion A
A1: ( [({}. A),({}. A)] `1 = {}. A & [({}. A),({}. A)] `2 = {}. A ) by MCART_1:7;

now

let x be Element of [:(Fin A),(Fin A):]; :: thesis: (FinPairUnion A) . [({}. A),({}. A)],x = x
thus (FinPairUnion A) . [({}. A),({}. A)],x = [({}. A),({}. A)] \/ x by Def6
.= x by A1, MCART_1:23 ; :: thesis: verum

end;

hence [({}. A),({}. A)] is_a_unity_wrt FinPairUnion A by BINOP_1:12; :: thesis: verum