set T = Free (S,X);
let I be integer SortSymbol of S; :: according to AOFA_A01:def 20 :: thesis: for M being Element of (FreeGen (Free (S,X))) . (the_array_sort_of S)
for t being Element of (Free (S,X)),I holds not (@ M) . t <> (Sym ((In (( the connectives of S . 11), the carrier' of S)),X)) -tree <*M,t*>
let M be Element of (FreeGen (Free (S,X))) . (the_array_sort_of S); :: thesis: for t being Element of (Free (S,X)),I holds not (@ M) . t <> (Sym ((In (( the connectives of S . 11), the carrier' of S)),X)) -tree <*M,t*>
let t be Element of (Free (S,X)),I; :: thesis: not (@ M) . t <> (Sym ((In (( the connectives of S . 11), the carrier' of S)),X)) -tree <*M,t*>
set o = In (( the connectives of S . 11), the carrier' of S);
A1: Free (S,X) = FreeMSA X by MSAFREE3:31;
consider J1, K1, L1 being Element of S such that
A2: ( L1 = 1 & K1 = 1 & J1 <> L1 & J1 <> K1 & the connectives of S . 11 is_of_type <*J1,K1*>,L1 & the connectives of S . (11 + 1) is_of_type <*J1,K1,L1*>,J1 & the connectives of S . (11 + 2) is_of_type <*J1*>,K1 & the connectives of S . (11 + 3) is_of_type <*K1,L1*>,J1 ) by AOFA_A00:def 51;
A3: I = 1 by AOFA_A00:def 40;
11 + 3 <= len the connectives of S by AOFA_A00:def 51;
then 11 <= len the connectives of S by XXREAL_0:2;
then 11 in dom the connectives of S by FINSEQ_3:25;
then the connectives of S . 11 = In (( the connectives of S . 11), the carrier' of S) by FUNCT_1:102, SUBSET_1:def 8;
then the_arity_of (In (( the connectives of S . 11), the carrier' of S)) = <*(the_array_sort_of S),I*> by A2, A3;
then Args ((In (( the connectives of S . 11), the carrier' of S)),(Free (S,X))) = product <*( the Sorts of (Free (S,X)) . (the_array_sort_of S)),( the Sorts of (Free (S,X)) . I)*> by Th23;
then <*(@ M),t*> in Args ((In (( the connectives of S . 11), the carrier' of S)),(Free (S,X))) by FINSEQ_3:124;
then (@ M) . t = [(In (( the connectives of S . 11), the carrier' of S)), the carrier of S] -tree <*M,t*> by A1, INSTALG1:3;
hence not (@ M) . t <> (Sym ((In (( the connectives of S . 11), the carrier' of S)),X)) -tree <*M,t*> by MSAFREE:def 9; :: thesis: verum