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:77; :: thesis: verum