let X be non empty disjoint_with_NAT set ; for C1, C2, I1, I2, J1, J2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st if-then-else (C1,I1,I2) = if-then-else (C2,J1,J2) holds
( C1 = C2 & I1 = J1 & I2 = J2 )
set S = ECIW-signature ;
set A = FreeUnivAlgNSG (ECIW-signature,X);
let C1, C2, I1, I2, J1, J2 be Element of (FreeUnivAlgNSG (ECIW-signature,X)); ( if-then-else (C1,I1,I2) = if-then-else (C2,J1,J2) implies ( C1 = C2 & I1 = J1 & I2 = J2 ) )
A1:
if-then-else (C1,I1,I2) = 3 -tree <*C1,I1,I2*>
by Th63;
if-then-else (C2,J1,J2) = 3 -tree <*C2,J1,J2*>
by Th63;
then
( if-then-else (C1,I1,I2) = if-then-else (C2,J1,J2) implies <*C1,I1,I2*> = <*C2,J1,J2*> )
by A1, TREES_4:15;
hence
( if-then-else (C1,I1,I2) = if-then-else (C2,J1,J2) implies ( C1 = C2 & I1 = J1 & I2 = J2 ) )
by FINSEQ_1:78; verum