let A be non-empty with_empty-instruction with_catenation unital UAStr ; for I being Element of A holds
( (EmptyIns A) \; I = I & I \; (EmptyIns A) = I )
let I be Element of A; ( (EmptyIns A) \; I = I & I \; (EmptyIns A) = I )
consider f being non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of A *), the carrier of A such that
A1:
f = the charact of A . 2
and
A2:
(Den ((In (1,(dom the charact of A))),A)) . {} is_a_unity_wrt f
by Def15;
A3:
2 in dom the charact of A
by Def11;
arity f = 2
by COMPUT_1:def 21;
then A4:
dom f = 2 -tuples_on the carrier of A
by COMPUT_1:22;
A5:
In (2,(dom the charact of A)) = 2
by A3, SUBSET_1:def 8;
<*I,I*> in dom f
by A4, FINSEQ_2:137;
hence
( (EmptyIns A) \; I = I & I \; (EmptyIns A) = I )
by A1, A2, A5; verum