let A be set ; :: thesis: {}. A is_a_unity_wrt FinUnion A
thus for x being Element of Fin A holds (FinUnion A) . (({}. A),x) = x :: according to BINOP_1:def 7,BINOP_1:def 16 :: thesis: {}. A is_a_right_unity_wrt FinUnion A

proof

let x be Element of Fin A; :: thesis: (FinUnion A) . (({}. A),x) = x
thus (FinUnion A) . (({}. A),x) = {} \/ x by Def4
.= x ; :: thesis: verum

end;

let x be Element of Fin A; :: according to BINOP_1:def 17 :: thesis: (FinUnion A) . (x,({}. A)) = x
thus (FinUnion A) . (x,({}. A)) = x \/ {} by Def4
.= x ; :: thesis: verum