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 binary 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 26;
then A4:
dom f = 2 -tuples_on the carrier of A
by COMPUT_1:25;
A5:
In 2,(dom the charact of A) = 2
by A3, FUNCT_7:def 1;
<*I,I*> in dom f
by A4, FINSEQ_2:157;
hence
( (EmptyIns A) \; I = I & I \; (EmptyIns A) = I )
by A1, A2, A5, Def1; verum