let X be non empty disjoint_with_NAT set ; for C, I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds if-then-else (C,I1,I2) = 3 -tree <*C,I1,I2*>
set S = ECIW-signature ;
reconsider s = ECIW-signature as non empty FinSequence of omega ;
set A = FreeUnivAlgNSG (ECIW-signature,X);
let C, I1, I2 be Element of (FreeUnivAlgNSG (ECIW-signature,X)); if-then-else (C,I1,I2) = 3 -tree <*C,I1,I2*>
A1:
3 in dom the charact of (FreeUnivAlgNSG (ECIW-signature,X))
by Def12;
reconsider f = the charact of (FreeUnivAlgNSG (ECIW-signature,X)) . 3 as non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) *), the carrier of (FreeUnivAlgNSG (ECIW-signature,X)) by Def12;
A2:
f = FreeOpNSG (3,ECIW-signature,X)
by A1, FREEALG:def 11;
A3:
3 in dom ECIW-signature
by Th54;
then
s /. 3 = ECIW-signature . 3
by PARTFUN1:def 6;
then A4:
dom (FreeOpNSG (3,ECIW-signature,X)) = 3 -tuples_on (TS (DTConUA (ECIW-signature,X)))
by A3, Th54, FREEALG:def 10;
A5:
<*C,I1,I2*> in 3 -tuples_on (TS (DTConUA (ECIW-signature,X)))
by FINSEQ_2:139;
thus if-then-else (C,I1,I2) =
f . <*C,I1,I2*>
by A1, SUBSET_1:def 8
.=
(Sym (3,ECIW-signature,X)) -tree <*C,I1,I2*>
by A2, A3, A4, A5, FREEALG:def 10
.=
3 -tree <*C,I1,I2*>
by A3, FREEALG:def 9
; verum