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