let X be non empty disjoint_with_NAT set ; :: thesis: 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)); :: thesis: ( 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; :: thesis: verum