let X be non empty disjoint_with_NAT set ; :: thesis: for I1, I2, J1, J2 being Element of (FreeUnivAlgNSG ECIW-signature ,X) st I1 \; I2 = J1 \; J2 holds
( I1 = J1 & I2 = J2 )
set S = ECIW-signature ;
set A = FreeUnivAlgNSG ECIW-signature ,X;
let I1, I2, J1, J2 be Element of (FreeUnivAlgNSG ECIW-signature ,X); :: thesis: ( I1 \; I2 = J1 \; J2 implies ( I1 = J1 & I2 = J2 ) )
A1: I1 \; I2 = 2 -tree I1,I2 by Th59;
J1 \; J2 = 2 -tree J1,J2 by Th59;
then ( I1 \; I2 = J1 \; J2 implies <*I1,I2*> = <*J1,J2*> ) by A1, TREES_4:15;
hence ( I1 \; I2 = J1 \; J2 implies ( I1 = J1 & I2 = J2 ) ) by FINSEQ_1:98; :: thesis: verum