defpred S1[ 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 S1[m,x]
proof
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 S1[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 S1[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 ;
len the charact of U1 = len the charact of U2 by ;
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 ;
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: S1[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;
consider p being FinSequence of PFuncs (([: the carrier of U1, the carrier of U2:] *),[: the carrier of U1, the carrier of U2:]) such that
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
S1[m,p . m] from 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 ; :: 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