let A be set ; :: thesis: for x being Element of [:(Fin A),(Fin A):] holds the_unity_wrt (FinPairUnion A) c= x
let x be Element of [:(Fin A),(Fin A):]; :: thesis: the_unity_wrt (FinPairUnion A) c= x
[({}. A),({}. A)] is_a_unity_wrt FinPairUnion A by Th36;
then the_unity_wrt (FinPairUnion A) = [{},{}] by BINOP_1:def 8;
then ( (the_unity_wrt (FinPairUnion A)) `1 = {} & (the_unity_wrt (FinPairUnion A)) `2 = {} ) by MCART_1:7;
hence ( (the_unity_wrt (FinPairUnion A)) `1 c= x `1 & (the_unity_wrt (FinPairUnion A)) `2 c= x `2 ) by XBOOLE_1:2; :: according to NORMFORM:def 1 :: thesis: verum