let A be set ; :: thesis: [({}. A),({}. A)] is_a_unity_wrt FinPairUnion A

now :: thesis: for x being Element of [:(Fin A),(Fin A):] holds (FinPairUnion A) . ([({}. A),({}. A)],x) = x

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 MCART_1:21 ; :: thesis: verum

end;

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