let Sigma be SigmaField of {1,2,3,4}; :: thesis: for I being set st I = {1,2,3} & Sigma = bool {1,2,3,4} holds
ex MyFunc being ManySortedSigmaField of I,Sigma st
( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} )
let I be set ; :: thesis: ( I = {1,2,3} & Sigma = bool {1,2,3,4} implies ex MyFunc being ManySortedSigmaField of I,Sigma st
( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} ) )
assume ASS2: ( I = {1,2,3} & Sigma = bool {1,2,3,4} ) ; :: thesis: ex MyFunc being ManySortedSigmaField of I,Sigma st
( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} )
deffunc H₁( Element of {1,2,3}) -> Subset of (bool {1,2,3,4}) = Set2_of_SigmaField3 $1;
consider fI1 being Function of {1,2,3},(bool (bool {1,2,3,4})) such that
A1: for d being Element of {1,2,3} holds fI1 . d = H₁(d) from FUNCT_2:sch 4();
reconsider fI1 = fI1 as Function of I,(bool Sigma) by ASS2;
reconsider El1 = 1 as Element of {1,2,3} by ENUMSET1:def 1;
A20: fI1 . 1 = Set2_of_SigmaField3 El1 by A1;
F1: Set2_of_SigmaField3 El1 = Set1_of_SigmaField3 El1 by Def9;
reconsider El1 = 2 as Element of {1,2,3} by ENUMSET1:def 1;
A200: fI1 . 2 = Set2_of_SigmaField3 El1 by A1;
F2: Set2_of_SigmaField3 El1 = Set1_of_SigmaField3 El1 by Def9;
reconsider El1 = 3 as Element of {1,2,3} by ENUMSET1:def 1;
A2: fI1 . 3 = Set2_of_SigmaField3 El1 by A1;
reconsider fI1 = fI1 as Function of I,(bool Sigma) ;
for i being set st i in I holds
fI1 . i is SigmaField of {1,2,3,4}

proof

let i be set ; :: thesis: ( i in I implies fI1 . i is SigmaField of {1,2,3,4} )
assume B1: i in I ; :: thesis: fI1 . i is SigmaField of {1,2,3,4}
fI1 . i is SigmaField of {1,2,3,4}

proof

per cases ( i = 1 or i = 2 or i = 3 ) by B1, ASS2, ENUMSET1:def 1;

suppose i = 1 ; :: thesis: fI1 . i is SigmaField of {1,2,3,4}

hence fI1 . i is SigmaField of {1,2,3,4} by F1, Def8, A20; :: thesis: verum

end;

suppose i = 2 ; :: thesis: fI1 . i is SigmaField of {1,2,3,4}

hence fI1 . i is SigmaField of {1,2,3,4} by F2, Def8, A200; :: thesis: verum

end;

suppose i = 3 ; :: thesis: fI1 . i is SigmaField of {1,2,3,4}

hence fI1 . i is SigmaField of {1,2,3,4} by Def9, A2; :: thesis: verum

end;

end;

end;

hence fI1 . i is SigmaField of {1,2,3,4} ; :: thesis: verum

end;

then reconsider fI1 = fI1 as ManySortedSigmaField of I,Sigma by KOLMOG01:def 2;
take fI1 ; :: thesis: ( fI1 . 1 = Special_SigmaField1 & fI1 . 2 = Special_SigmaField2 & fI1 . 3 = Trivial-SigmaField {1,2,3,4} )
thus ( fI1 . 1 = Special_SigmaField1 & fI1 . 2 = Special_SigmaField2 & fI1 . 3 = Trivial-SigmaField {1,2,3,4} ) by F1, Def8, A20, F2, A200, Def9, A2; :: thesis: verum