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

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