defpred S_{1}[ Nat, set ] means for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1

for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . $1 & h2 = the charact of U2 . $1 holds

$2 = [[:h1,h2:]];

set l = len the charact of U1;

set c = [: the carrier of U1, the carrier of U2:];

A2: dom the charact of U2 = Seg (len the charact of U2) by FINSEQ_1:def 3;

A3: Seg (len the charact of U1) = dom the charact of U1 by FINSEQ_1:def 3;

A4: for m being Nat st m in Seg (len the charact of U1) holds

ex x being Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) st S_{1}[m,x]

A6: dom p = Seg (len the charact of U1) and

A7: for m being Nat st m in Seg (len the charact of U1) holds

S_{1}[m,p . m]
from FINSEQ_1:sch 5(A4);

reconsider p = p as PFuncFinSequence of [: the carrier of U1, the carrier of U2:] ;

take p ; :: thesis: ( len p = len the charact of U1 & ( for n being Nat st n in dom p holds

for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1

for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds

p . n = [[:h1,h2:]] ) )

thus len p = len the charact of U1 by A6, FINSEQ_1:def 3; :: thesis: for n being Nat st n in dom p holds

for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1

for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds

p . n = [[:h1,h2:]]

let n be Nat; :: thesis: ( n in dom p implies for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1

for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds

p . n = [[:h1,h2:]] )

assume n in dom p ; :: thesis: for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1

for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds

p . n = [[:h1,h2:]]

hence for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1

for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds

p . n = [[:h1,h2:]] by A6, A7; :: thesis: verum

for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . $1 & h2 = the charact of U2 . $1 holds

$2 = [[:h1,h2:]];

set l = len the charact of U1;

set c = [: the carrier of U1, the carrier of U2:];

A2: dom the charact of U2 = Seg (len the charact of U2) by FINSEQ_1:def 3;

A3: Seg (len the charact of U1) = dom the charact of U1 by FINSEQ_1:def 3;

A4: for m being Nat st m in Seg (len the charact of U1) holds

ex x being Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) st S

proof

consider p being FinSequence of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) such that
let m be Nat; :: thesis: ( m in Seg (len the charact of U1) implies ex x being Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) st S_{1}[m,x] )

assume A5: m in Seg (len the charact of U1) ; :: thesis: ex x being Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) st S_{1}[m,x]

then reconsider f1 = the charact of U1 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by A3, MARGREL1:def 24;

len the charact of U1 = len the charact of U2 by A1, UNIALG_2:1;

then reconsider f2 = the charact of U2 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 by A2, A5, MARGREL1:def 24;

reconsider F = [[:f1,f2:]] as Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) by PARTFUN1:45;

take F ; :: thesis: S_{1}[m,F]

let h1 be non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1; :: thesis: for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . m & h2 = the charact of U2 . m holds

F = [[:h1,h2:]]

let h2 be non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2; :: thesis: ( h1 = the charact of U1 . m & h2 = the charact of U2 . m implies F = [[:h1,h2:]] )

assume ( h1 = the charact of U1 . m & h2 = the charact of U2 . m ) ; :: thesis: F = [[:h1,h2:]]

hence F = [[:h1,h2:]] ; :: thesis: verum

end;assume A5: m in Seg (len the charact of U1) ; :: thesis: ex x being Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) st S

then reconsider f1 = the charact of U1 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1 by A3, MARGREL1:def 24;

len the charact of U1 = len the charact of U2 by A1, UNIALG_2:1;

then reconsider f2 = the charact of U2 . m as non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 by A2, A5, MARGREL1:def 24;

reconsider F = [[:f1,f2:]] as Element of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) by PARTFUN1:45;

take F ; :: thesis: S

let h1 be non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1; :: thesis: for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . m & h2 = the charact of U2 . m holds

F = [[:h1,h2:]]

let h2 be non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2; :: thesis: ( h1 = the charact of U1 . m & h2 = the charact of U2 . m implies F = [[:h1,h2:]] )

assume ( h1 = the charact of U1 . m & h2 = the charact of U2 . m ) ; :: thesis: F = [[:h1,h2:]]

hence F = [[:h1,h2:]] ; :: thesis: verum

A6: dom p = Seg (len the charact of U1) and

A7: for m being Nat st m in Seg (len the charact of U1) holds

S

reconsider p = p as PFuncFinSequence of [: the carrier of U1, the carrier of U2:] ;

take p ; :: thesis: ( len p = len the charact of U1 & ( for n being Nat st n in dom p holds

for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1

for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds

p . n = [[:h1,h2:]] ) )

thus len p = len the charact of U1 by A6, FINSEQ_1:def 3; :: thesis: for n being Nat st n in dom p holds

for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1

for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds

p . n = [[:h1,h2:]]

let n be Nat; :: thesis: ( n in dom p implies for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1

for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds

p . n = [[:h1,h2:]] )

assume n in dom p ; :: thesis: for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1

for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds

p . n = [[:h1,h2:]]

hence for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1

for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds

p . n = [[:h1,h2:]] by A6, A7; :: thesis: verum