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 Th17;
then the_unity_wrt (FinPairUnion A) = [{},{}] by BINOP_1:def 8;
then ( (the_unity_wrt (FinPairUnion A)) `1 = {} & (the_unity_wrt (FinPairUnion A)) `2 = {} ) ;
hence ( (the_unity_wrt (FinPairUnion A)) `1 c= x `1 & (the_unity_wrt (FinPairUnion A)) `2 c= x `2 ) ; :: according to NORMFORM:def 1 :: thesis: verum